Lecture Notes on Categorical Judgments
Frank Pfenning · 2010
In addition, we have considered hypothetical judgments J1, . . . , Jn ` J in general, and x1:A1, . . . , xn:An `M : C in particular. A few crucial properties of these systems are still outstanding. In particular, we still need to prove global versions of the local soundness and completeness properties. We call them here internal soundess and completeness to remind us that they refer to properties of proofs and verifications, rather than to any external semantics in terms of mathematical structures.