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

Definition

A cone type on a type $A$ is a higher inductive type $Cone(A)$ inductively generated by

• A term $e:Cone(A)$

• A function $i: A \to Cone(A)$

• A term

All cone types are contractible, and therefore could be though of as a way of constructing free contractible types for any type $A$.

Examples

• The unit type is a cone type on the empty type.

• The interval type is a cone type on the unit type.

See also

• contractible type

• proposition

• higher inductive type