In Luo's type-theoretical semantics of natural language, he represents, for example, the verb "talk" as having this type:
$talk: Human \to Prop$
Unfortunately, Luo doesn't expand much on this. If I get it right, the term "talk" comes from the abstraction rule for $\Pi$-types:
$ \ \cfrac{\Gamma, x: \text{Human} \vdash p: \text{Prop}}{\Gamma \vdash \lambda x:\text{Human}.p: \Pi x:\text{Human}.\text{Prop}} \ $
(where $talk = \lambda x:\text{Human}.p$). And then, to get the proposition "A man talks", we apply the application rule (if that's the right name) for $\Pi$-types:
$ \ \cfrac{\Gamma \vdash talk: \Pi x:\text{Human}.\text{Prop},\ \Gamma \vdash m:\text{Human}}{\Gamma \vdash talk(m): \text{Prop}} \ $
(where $talk(m) = p$).
But the top line of the first derivation already contains $\Gamma, x: \text{Human} \vdash p: \text{Prop}$ as a premise. I suppose it's not derivable from anything and has to be postulated as an axiom? It looks weird (or tautological) that we need to assume that $p:\text{Prop}$ just to prove at the end that $talk(m)$, which is equal to $p$, has type $\text{Prop}$.
Perhaps the frist derivation shouldn't be considered at all, and we just need to postulate that there exists an inhabitant of type $\Pi x:\text{Human}.\text{Prop}$, and this inhabitant is called $talk$? This should solve the problem with postulating $p:\text{Prop}$.
There are several ways to do this.
From the modern viewpoint, the most natural way is to add a rule: $$\frac{\Gamma \vdash h : \textrm{Human}}{\Gamma \vdash \textsf{talk}(h) : \textrm{Prop}}$$ Note that it is not a function! We can create an expression of the function type by using the abstraction rule $\lambda x. \textsf{talk}(x)$. This is the most natural, because it does not unnecessarily rely on function types. Rather, it only depends on the structure of type theory itself. So even if we consider type theories without function types, this rule still makes sense.
Next, we can add an axiom, which is a rule of the form $$\frac{}{\Gamma \vdash \textsf{c} : A}$$ where $A$ has no free variables. In this case we are adding $\textsf{talk} : \textrm{Human} \to \textrm{Prop}$. Or we can write that as $\Pi x{:} \textrm{Human}. \textrm{Prop}$. Even though there are no variables involved, we have to include the $\Gamma$ in that rule. Otherwise it breaks substitution.
As another way, we can consider $\Gamma$ of the form $\textit{talk}:\textrm{Human} \to \textrm{Prop}, \Gamma'$. Now we can treat $\textit{talk}$ as just another variable. This is equivalent to adding an axiom. The benefit of this is you don't have to add any more rules or axioms, and everything takes place in the original type theory.