If I understand correctly, part of the buzz surrounding homotopy type theory is that a small system of axioms ends up producing all of the (weak) $\infty$-groupoid axioms, where by an "axiom" in this context I really mean a pair $(k,f)$ where $k \in \mathbb{N}$ and $f$ is a $k$-cell. This includes all relevant associators, pentagon identities etc. I think these are called "coherence laws" in a nutshell, but I'm not sure.

Anyway, is there a simple system, much weaker than homotopy type theory, that also produces all these axioms?

For example, if I want to investigate the algebraic theory generated by an $\infty$-groupoid $X$ together with a function $f : X \rightarrow X$ and an isomorphism $\alpha : f \circ f \rightarrow \mathrm{id}_X$, such a system ought to tell me all the relevant laws.

  • $\begingroup$ Doubt it. The closest you can get outside of homotopy type theory, as far as I know, is algebraic Kan complexes, but that's very much giving a generating set of axioms, not the complete list, and they're not the nice familiar globular axioms either. Globular $\infty$-groupoids seem to rely on some non-canonical choices like a Batanin globular operad. $\endgroup$ – Kevin Carlson Dec 15 '18 at 22:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.