Homotopy Type Theory proposition > history (Rev #2)

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.

Homotopy Type Theory proposition > history (Rev #2)

Idea

Definition

Examples

See also