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
homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
In homotopy type theory, a suspension type of any type $X$ is the pushout type of the terminal function $X \to \ast$ (to the unit type) along itself, hence the pushout of the span $\ast \longleftarrow X \longrightarrow \ast$.
The categorical semantics is given by suspension objects in homotopy theory (and hence by suspension of topological spaces in, say, the classical model structure on topological spaces).
As a higher inductive type, the (unreduced) suspension $\mathrm{S} X$ of a type $X$ is generated by
A term $\mathrm{nth} \colon \mathrm{S} X$
a term $\mathrm{sth} \colon \mathrm{S} X$
A function $mer \colon X \to Id_{\mathrm{S}X}\big(nth,\, sth\big)$
(to the identity type of $\mathrm{S}X$).
(graphics adapted from Muro 2010)
The resulting inference rules are the specialization of those of pushout types (see there).
In Coq pseudocode this becomes
Inductive Suspension (X \colon Type) : Type
| nth : Suspension X
| sth : Suspension X
| mer : X -> Id Suspension X nth sth
This says that the type is dependent on the type $X$ 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 $X$ 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}$.
suspension type, reduced suspension type
Last revised on January 5, 2023 at 18:59:48. See the history of this page for a list of all contributions to it.