|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-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|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, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
In type theory, the paradigm of propositions as types says that propositions and types are essentially the same. A proposition is identified with the type (collection) of all its proofs, and a type is identified with the proposition that it has a term (so that each of its terms is in turn a proof of the corresponding proposition).
… to show that a proposition is true in type theory corresponds to exhibiting an element term of the type corresponding to that proposition. We regard the elements of this type as evidence or witnesses that the proposition is true. (They are sometimes even called proofs… (from Homotopy Type Theory -- Univalent Foundations of Mathematics, section 1.11)
Not all type theories follow this paradigm; among those that do, Martin-Löf type theories are the most famous. In its variant as homotopy type theory the paradigm is also central, but receives some refinements, see at Propositions as some types
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 Brouwer-Heyting-Kolmogorov interpretation. 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 corresponds 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 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 .
A standard account for intuitionistic type theory is
Discussion in homotopy type theory is in section 1.11 of
Exposition is in
An influential original article was
The origins of this manuscript and its publication are recounted in a 2014 email from Howard to Philip Wadler:
This influential note brought Dana Scott to write “Constructive Validity” (a precursor of type theory) and also strongly influenced Per Martin-Löf. Independently and at about the same time, the idea was also found by N.G. de Bruijn? for the Automath system.
Also William Lawvere was there, lecturing on hyperdoctrines. Lawvere told Steve Awodey that the basic example of a morphism of hyperdoctrines from the proof-relevant one to the proof-irrelevant one was influenced by Kreisel, not Howard, who attended Lawvere’s Chicago lectures in the 60s. See pages 2 and 3 of
But the story started earlier with what has been called the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, highlighted for instance in (Troelstra 91), which identifies a proposition with the collection of its proofs. This view goes back to an observation of Kolmogorov that the formalisation of Brouwer’s ideas by Heyting in 1930 can be semantically interpreted as a calculus of ‘Aufgaben’ - problems (and solutions), reported in
A historical account is in the section on types in
and in section 5 of
Philip Wadler is currently in the process of writing another history: