symmetric monoidal (∞,1)-category of spectra
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
A symmetric ring groupoid is a 1-truncated $E_\infty$-ring.
Equivalently: A groupoid $G$ that is both a symmetric 2-group $(G, 0, \oplus)$ and a symmetric monoidal groupoid $(G, 1, \otimes)$ such that $\otimes$ distributes over $\oplus$ satisfying certain higher coherence laws (given in Kelly74).
The discrete groupoid of integers $\mathbb{Z}$ is the initial symmetric ring groupoid.
The contractible groupoid or the trivial ring groupoid $0$ is the terminal symmetric ring groupoid.
Last revised on May 18, 2022 at 12:17:43. See the history of this page for a list of all contributions to it.