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-monoid?/-space. In category theory, a magmoidal groupoid with unit with an associator but no higher coherence laws.
In intensional type theory with function extensionality, a groupoid is a 1-truncated type and a H-monoidal groupoid or -spatial groupoid is a groupoid that is also an H-monoid?/-space.
In category theory, a H-monoidal groupoid or -spatial groupoid is a magmoidal groupoid with unit with unital associator natural isomorphisms .
Last revised on July 14, 2022 at 08:53:51. See the history of this page for a list of all contributions to it.