|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
In type theory, the paradigm of propositions as types says that a proposition and a type are the same thing. A proposition is identified with its type of proofs, and a type is identified with the proposition that it has a term.
Not all type theories follow this paradigm; among those that do, Martin-Löf type theories are the most famous.
Even when the paradigm is not adopted, however, there is still a close relationship between logical and type-theoretic operations, called the Curry–Howard isomorphism or (if it is not clear in which category this isomorphism is supposed to exist) the Curry–Howard correspondence. Or maybe better (Harper) the BHK correspondence. This correspondence is most precise and well-developed for intuitionistic logic.
Accordingly, logical operations on propositions have immediate analogs on types. For instance logical and coresponds to forming the product type (a proof of and a proof of ), the universal quantifier corresponds to dependent product, the existential quantifier to dependent sum.
A related paradigm may be called propositions as some types, in which propositions are identified with particular types, but not all types are regarded as propositions. Generally, the propositions are the “types with at most one term”. This is the paradigm usually used in the internal logic of categories such as toposes, as well as in homotopy type theory. In this case, the type-theoretic operations on types either restrict to the propositions to give logical operations (for conjunction, implication, and the universal quantifier), or have to be “reflected” therein (for disjunction and the existential quantifier). The reflector operation is called a bracket type.
the objects of are proofs of some proposition;
the morphisms of are equivalences between these proofs;
the 2-morphisms of are equivalences between these equivalences, and so on.
if is 0-truncated then there may be more than one proof, but none equivalent to itself in an interesting way;
if is 1-truncated then there may be proofs of the corresponding proposition that are equivalent to themselves in interesting ways.
We would not say homotopy type theory has propositions as types in the same way that Martin–Löf type theory has; only the -truncated types are propositions as such. That is, in HoTT we have propositions as some types. In this case the bracket types can be identified with a particular higher inductive type called .
Per Martin-Löf, Intuitionistic Type Theory, Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Napoli, 1984.
W. W. Tait. The completeness of intuitionistic first-order logic. Unpublished manuscript.