natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The cone type is an axiomatization of the cone in the context of homotopy type theory.
A cone type on a type is a higher inductive type inductively generated by
A term
A function
A term
In Coq pseudocode, the cone is given by
Inductive Cone (A : Type) : Type
| vertex : Cone A
| base : A -> Cone A
| edge : A -> Id Cone A vertex base(a)
It can equivalently be defined as the (homotopy) pushout of and the unit type under . This definition makes it clear that the cone type is always a contractible type. As a result, cone types could be though of as a way of constructing free contractible types for any type .
The unit type is the cone type of an empty type .
The interval type is the cone type of the unit type
A simplex type? is the cone type of the simplex type . and .
Last revised on June 16, 2022 at 11:58:14. See the history of this page for a list of all contributions to it.