< [[nlab:cone type]] ## 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 $$p: \prod_{a:A} e = i(a)$$ 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]] category: not redirected to nlab yet