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 suspension type is an axiomatization of the suspension object in the context of homotopy type theory.
As a higher inductive type, the suspension $\Sigma A$ of a type $A$ is given by
In Coq pseudocode it becomes
Inductive Suspension (A : Type) : Type
| north : Suspension A
| south : Suspension A
| meridian : A -> Id Suspension A north south
This says that the type is dependent on the type A and inductive constructed from two terms in the suspension, whose interpretation is as the north and south poles of the suspension, together with a term in the function type from A to the identity type of paths between these two terms, representing the meridians from the north to the south pole.
The two-valued type $\mathbf{2}$ is the suspension type of the empty type $\mathbf{0}$.
The interval type $I$ is the suspension type of the unit type $\mathbf{1}$.
The circle type $S^1$ is the suspension type of $\mathbf{2}$.
The homotopical disk type $G_2$ is the suspension type of $I$.
Homotopical $n$-sphere types of dimension $n:\mathbb{N}$, $S^n$, are suspension types of $S^{n-1}$.
Homotopical $n$-globe types of dimension $n:\mathbb{N}$, $G_n$, are suspension types of $G_{n-1}$.
In general, the suspension type $\Sigma A$ of a type $A$ is the homotopy pushout of the span $\mathbf{1} \leftarrow A \rightarrow \mathbf{1}$.
suspension type
Last revised on June 7, 2022 at 22:13:16. See the history of this page for a list of all contributions to it.