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 $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
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 $A$ and the unit type $1$ under $A$. 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 $A$.
The unit type $1$ is the cone type of an empty type $0$.
The interval type $I$ is the cone type of the unit type $1$
A simplex type? $\Delta_n$ is the cone type of the simplex type $\Delta_{n-1}$. $\Delta_1 = I$ and $\Delta_0 = 1$.
Last revised on June 16, 2022 at 11:58:14. See the history of this page for a list of all contributions to it.