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

Showing changes from revision #1 to #2: Added | Removed | Changed

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 every identity type in$A$ is a proposition follows from concatenation and inverses of identity types.

There The above definition could be reworded in natural language as a type that is also inhabited and a fourth proposition; definition i.e. of contractible types 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