## Idea A type which represents the notion of truth value in homotopy type theory. ## Definition A __proposition__ is a type $A$ with a term $$p: \prod_{a:A} \prod_{b:A} a = b$$ Since a proposition is either empty or contractible, there is another definition of a proposition as a type $A$ with a term $$p: A \rightarrow 0 + isContr(a=b)$$ 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 $$p: A \rightarrow isContr(a=b)$$ 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 $$\tau_{-1}: \prod_{a:A} \prod_{b:A} isContr(a=b)$$ and a fifth definition as a type $A$ with a term $$p: \prod_{a:A} \prod_{b:A} a = b$$ and a term $$c: \prod_{d:\prod_{a:A} \prod_{b:A}} p = d$$ ## Examples * The [[empty type]] is a proposition. * Every [[contractible type]] is a proposition. ## See also * [[predicate]] * [[contractible type]] * [[set]] * [[homotopy level]]