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
monoid theory in algebra:
categorification
monoid theory in algebra:
Invoking the homotopy hypothesis, we define a $k$-tuply monoidal $n$-groupoid to be an $E_k$-$n$-truncated type: a topological space which is a homotopy n-type and which is equipped with an action by the little k-cubes operad (or some operad equivalent to it).
There is a periodic table of $k$-tuply monoidal $n$-groupoids:
$k$↓\$n$→ | $-1$ | $0$ | $1$ | $2$ | ... | $\infty$ |
---|---|---|---|---|---|---|
$0$ | trivial | pointed set | pointed groupoid | pointed 2-groupoid | ... | pointed ∞-groupoid |
$1$ | trivial | monoid | monoidal groupoid | monoidal 2-groupoid? | ... | A-∞-space/E1-algebra |
$2$ | \" | commutative monoid | braided monoidal groupoid | braided monoidal 2-groupoid? | ... | E2-algebra |
$3$ | \" | \" | symmetric monoidal groupoid | sylleptic monoidal 2-groupoid? | ... | E3-algebra |
$4$ | \" | \" | \" | symmetric monoidal 2-groupoid? | ... | E4-algebra |
⋮ | \" | \" | \" | \" | ⋱ | ⋮ |
$\infty$ | trivial | commutative monoid | symmetric monoidal groupoid | symmetric monoidal 2-groupoid? | ... | E-∞-algebra |
Last revised on May 16, 2022 at 15:34:16. See the history of this page for a list of all contributions to it.