A type which represents the notion of truth value in homotopy type theory.
A proposition is a type with a term
Since a proposition is either empty or contractible, there is another definition of a proposition as a type 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 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 with a term
and a fifth definition as a type with a term
and a term
The empty type is a proposition.
Every contractible type is a proposition.