symmetric monoidal (∞,1)-category of spectra
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
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
categorification
In homotopy type theory, a 1-truncated H-space/$A_2$-space. In category theory, the groupoidal categorification of a unital magma.
In intensional type theory with function extensionality, a groupoid is a 1-truncated type and a H-spatial groupoid, $A_2$-spatial groupoid, unital magmoidal groupoid, or magmoidal groupoid with unit is a groupoid that is also an H-space/$A_2$-space.
In category theory, a unital magmoidal groupoid or magmoidal groupoid with unit is a magmoidal groupoid $(G, \otimes)$ with a unit $I$ and natural unitary isomorphisms $\lambda_A \colon A\otimes I \simeq^\dagger A$ and $\rho_A \colon I\otimes A \simeq^\dagger A$.
Last revised on July 14, 2022 at 08:58:14. See the history of this page for a list of all contributions to it.