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

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

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 \to 0 + isContractible isContr (a = b)

p: A \rightarrow 0 + ~~isContractible(a=b)~~ 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 \to isContractible isContr (a = b)

p: A \rightarrow ~~isContractible(a=b)~~ 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

τ_{- 1} : \prod_{a : A} \prod_{b : A} isContractible isContr (a = b)

\tau_{-1}: \prod_{a:A} \prod_{b:A} ~~isContractible(a=b)~~ 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, changes)

Idea

Definition

Examples

See also