Homotopy Type Theory contractible type > history (Rev #3)

Idea

A type which represents the notion of logical truth in homotopy type theory.

Definitions

A contractible type is a type $A$ with a term

c: \sum_{a:A} \prod_{b:A} a = b

Since contractible types are inhabited propositions, there is an alternate definition of contractible type as a type $A$ with a point $e:A$ and a term

p: isProp(A)

The above term could be replaced with the following instead:

p: \prod_{a:A} a = e

and that $A$ is a proposition follows from concatenation and inverses of identity types.

The above definition could be reworded in natural language as a type that is inhabited and a proposition; i.e. as a type $A$ with a term

c: A \times isProp(A)

Examples

The unit type? is a contractible type.
The interval type? is a contractible type.
By the third definition, every cone type is a contractible type, of which the unit type (cone type of the empty type) and the interval type (cone type of the unit type) are examples of cone types.

Homotopy Type Theory contractible type > history (Rev #3)

Idea

Definitions

Examples

See also