# Is there a “low-powered” axiom system for producing all the $\infty$-groupoid axioms?

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.

• 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. – Kevin Carlson Dec 15 '18 at 22:59