Homotopy Type Theory contractible type > history (Rev #4, changes)

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

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

The above term could be replaced with the following instead:

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

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.

See also

• proposition

• set