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, the notion of reduced suspension type is an axiomatization of the reduced suspension in pointed homotopy theory.
The underlying type of a pointed reduced suspension type is equivalent to the plain suspension type of the given underlying type, so that, up to equivalence one may simply take the reduced suspension to be the plain suspension equipped with any one of its terms as basepoint (e.g, UFP13, Rem. 8.6.3).
However, in practice it is sometimes convenient to use a different (even if equivalent) construction of the reduced suspension:
For a given type $X$, we follow the conventions of the reduced suspension article and write $\mathrm{S} X$ for the plain suspension type of $X$ and $\Sigma X$ for the reduced suspension type of $A$.
The reduced suspension type of a pointed type $(X,x)$ with basepoint term $x \colon X$ may be defined as the smash product type of the pointed circle type $(S^1, s)$ with $X$:
In cohesive homotopy type theory, let $(X, x)$ be a pointed cohesive type, and let $\mathbf{\Sigma} X$ be the reduced suspension of $X$, as a cohesive type. Then the reduced suspension type of $X$, as a discrete homotopy type, is the shape of the reduced suspension of $X$: $\Sigma X \coloneqq \esh(\mathbf{\Sigma} X)$.
In particular, if we take $(X, x)$ to be a pointed topological space in real-cohesive homotopy type theory, this allows a construction of reduced suspension types directly from reduced suspensions in classical algebraic topology.
The reduced suspension type of the $n$-sphere type $S^n$ is equivalent to the $(n + 1)$-sphere type $S^{n + 1}$
suspension type, reduced suspension type
Last revised on February 2, 2023 at 08:49:50. See the history of this page for a list of all contributions to it.