Homotopy Type Theory proposition > history (Rev #6, changes)

Since a proposition is either empty or contractible, there is another definition of a proposition as a type $A$ with a term

This could be reworded in natural language as a proposition is contractible if it is inhabited, which results in this definition of a proposition as a type $A$ with a term

Propositions are also (-1)-truncated types, i.e. types whose identity types are contractible, so there is a fourth definition of a proposition as a type $A$ with a term

and a fifth definition as a type $A$ with a term

and a term

Examples

• The empty type is a proposition.

• Every contractible type is a proposition.