A cone type on a type is a higher inductive type inductively generated by
A term
A function
A term
All cone types are contractible, and therefore could be though of as a way of constructing free contractible types for any type .
The unit type is a cone type on the empty type.
The interval type is a cone type on the unit type.