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

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

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