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 AA with a term

p: a:A b:Aa=bp: \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 AA with a term

p:A0+isContr(a=b)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 AA with a term

p:AisContr(a=b)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 AA with a term

τ 1: a:A b:AisContr(a=b)\tau_{-1}: \prod_{a:A} \prod_{b:A} isContr(a=b)

and a fifth definition as a type AA with a term

p: a:A b:Aa=bp: \prod_{a:A} \prod_{b:A} a = b

and a term

c: d: a:A b:Ap=dc: \prod_{d:\prod_{a:A} \prod_{b:A}} p = d

Examples

See also

Revision on February 13, 2022 at 22:39:17 by Anonymous?. See the history of this page for a list of all contributions to it.