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

61 Views Asked by At

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.