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 category theory, the notion of a magmoidal groupoid is the groupoidal categorification of the notion of magma, hence a magmoidal groupoid is simply a groupoid equipped with a “binary operation” on it. Similarly, under the relation between category theory and type theory, in homotopy type theory a magmoidal groupoid is a 1-truncated type equipped with a binary operation.
In intensional type theory with function extensionality, a groupoid is a 1-truncated type and a binary operation on a groupoid $G$ is a function $(-)\otimes (-) \colon G \times G \to G$ from the product groupoid $G \times G$ to $G$. A magmoidal groupoid $(G,\otimes)$ is a groupoid equipped with a binary operation on it.
In category theory, a groupoid is a dagger category where every morphism is unitary, and a binary operation on a groupoid $G$ is a dagger functor $(-)\otimes (-) \colon G \times G \to G$ from the product groupoid? $G \times G$ to $G$. A magmoidal groupoid $(G,\otimes)$ is a groupoid equipped with a binary operation on it.
Last revised on May 16, 2022 at 15:37:52. See the history of this page for a list of all contributions to it.