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 ring groupoid is a 1-truncated -ring.
Equivalently: A groupoid that is both a symmetric 2-group and a monoidal groupoid such that distributes over satisfying certain higher coherence laws (given in Kelly74).
The discrete groupoid of integers is the initial ring groupoid.
The contractible groupoid or the trivial ring groupoid is the terminal ring groupoid.
Last revised on May 20, 2022 at 20:29:15. See the history of this page for a list of all contributions to it.