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

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: \prod_{a:A} \prod_{b:A} a = b

The above term could be replaced with the following instead:

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

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

There is also a fourth definition of contractible types as a type $A$ with a term

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

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 #1)

Idea

Definitions

Examples

See also