nLab
propositions as types

Idea

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 an element.

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. 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 product types $A\times B$ (a proof of $A$ and a proof of $B$), the forall 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 inhabitant”. 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.

Curry–Howard in homotopy type theory

In homotopy type theory where types may be thought of as ∞-groupoids (or rather ∞-stacks, more generally), we may think for $A$ any type of

• the objects of $A$ are proofs of some proposition;

• the morphisms of $A$ are equivalences between these proofs;

• the 2-morphisms of $A$ are equivalences between these equivalences, and so on.

So in terms of the notion of n-connected and n-truncated objects in an (∞,1)-category we have

• if $A$ is (-1)-connected then the corresponding proposition is true;

• if $A$ is (-2)-truncated (a (-2)-groupoid) then the corresponding proposition is true by a unique proof which is uniquely equivalent to itself, etc.;

• if $A$ is (-1)-truncated (a (-1)-groupoid) then the corresponding proposition may be true or false, but if it is true it is to by a unique proof as above;

• if $A$ is 0-truncated then there may be more than one proof, but none equivalent to itself in an interesting way;

• if $A$ 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 $(-1)$-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 $\mathrm{isInhab}$.

Related concepts

• bracket types

• proofs as programs

References

The idea was originally developed in

• 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.