I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of semantics of an intransitive verb, which is $talk: Human \to Prop$, where $Prop$ is "the internal totality of all logical propositions" (I'm not sure what "internal totality" means, but maybe that's not exactly relevant here), with inference rules as shown below.
Now, if $j: Human$ ($j$ for "John"), then I believe in certain context we can prove that $talk(j): Prop$. But how do I find a term that would prove the proposition $talk(j)$? I'm not sure I understand even what such a term should look like.