For a while, Mike Shulman and I (and others) have wondered on and off whether it might be possible to represent all higher inductive types (i.e. with constructors of arbitrary dimension) using just 1-HIT’s (0- and 1-cell constructors only), somewhat analogously with the reduction of all standard inductive types to a few specific instances — W-types, Id-types, etc. Recently we realised that yes, it can be done, and quite prettily. It’s perhaps most easily explained in pictures: here are a couple of 2-cells, represented using just 0- and 1-cells:
And here’s a 3-cell, similarly represented:
As a topologist would say it: the (n+1)-disc is the cone on the n-sphere. To implement this logically, we first construct the spheres as a 1-HIT, using iterated suspension:
Inductive Sphere : Nat -> Type := | north (n:Nat) : Sphere n | south (n:Nat) : Sphere n | longitude (n:Nat) (x:Sphere n) : Paths (north (n+1)) (south (n+1)).
Then we define (it’s a little fiddly, but do-able) a way to, given any parallel pair s, t of n-cells in a space X, represent them as a map rep s t : Sphere n -> X. (I’m suppressing a bunch of implicit arguments for the lower dimensional sources/targets.)
Now, whenever we have an (n+1)-cell constructor in a higher inductive type
HigherInductive X : Type := (…earlier constructors…) | constr (a:A) : HigherPaths X (n+1) (constr_s a) (constr_t a) (…later constructors…)
we replace it by a pair of constructors
| constr_hub (a:A) : X | constr_spoke (a:A) (t : Sphere n) : Paths X (rep (s a) (t a)) (constr_hub a)
Assuming functional extensionality, we can give from this a derived term constr_derived : forall (a:A), HigherPaths (n+1) (constr_s a) (constr_t a); we use this for all occurences of constr in later constructors. The universal property of the modified HIT should then be equivalent to that of the original one.
(Here for readability X was non-dependent and constr had only one argument; but the general case has no essential extra difficulties.)
What can one gain from this? Again analogously with the traditional reduction of inductive types to a few special cases, the main use I can imagine is in constructing models: once you’ve modeled 1-HIT’s, arbitrary n-HIT’s then come for free. It also could be a stepping-stone for reducing yet further to a few specific 1-HIT’s… ideas, anyone?
On a side note, while I’m here I’ll take the opportunity to briefly plug two notes I’ve put online recently but haven’t yet advertised much:
- Model Structures from Higher Inductive Types, which pretty much does what it says on the tin: giving a second factorisation system on syntactic categories CT (using mapping cylinders for the factorisations), which along with the Gambino-Garner weak factorisation system gives CT much of the structure of a model category — all but the completeness and functoriality conditions. The weak equivalences are, as one would hope, the type-theoretic
Equivwe know and love. - Univalence in Simplicial Sets, joint with Chris Kapulkin and Vladimir Voevodsky. This gives essentially the homotopy-theoretic aspects of the construction of the univalent model in simplicial sets, and these aspects only — type theory isn’t mentioned. Specifically, the main theorems are the construction of a (fibrant) universe that (weakly) classifies fibrations, and the proof that it is (in a homotopy-theoretic sense) univalent. The results are not new, but are taken from Voevodsky’s Notes on Type Systems and Oberwolfach lectures, with some proofs modified; the aim here is to give an accessible and self-contained account of the material.
(Photos above by ne*, brandsvig, and JPott, via the flickr Creative Commons pool, licensed under CC-NonCom-Attrib-NoDerivs.)
Homotopy Type Theory 
Thanks for posting this! I’m really happy that we’ve got this nice simplification.
One thing you didn’t mention is that this reduction only respects the universal property propositionally: even if we had 1-HITs which satisfied definitional computation rules, then this construction would only produce n-HITs satisfying propositional computation rules (for higher path constructors). At least, unless you have some trick in mind that I’m not thinking of.
For purposes of constructing models, this may not be such a big deal, since it’s not yet clear to what extent we can build models of HITs with definitional computation rules at all (except for point-constructors). And of course it’s not clear either to what extent definitional computation rules for path-constructors even make sense, since writing one down involves making some arbitrary choices (so does the propositional computation rule, but the arbitrariness is less worrisome since making a different choice would only nudge things propositionally). But anyway, there it is.
Another related fact which we learned recently is that 1-HITs are not reducible to 0-HITs. This is not so much of a surprise by itself, but what may be a bit surprising is that it’s true already in extensional type theory, and even adding quotient types along with 0-HITs is insufficient. In fact, even ZF does not suffice to construct all 1-HITs!
In extensional type theory, of course, n-HITs for n > 1 are not very interesting, and 1-HITs are a bit degenerate, but they are still interesting. What 1-HITs allow you to do in an extensional theory is to inductively define a set and quotient it by an equivalence relation at the same time. For instance, with 1-HITs we can build free algebras for any algebraic theory, using 0-cell constructors to put in the operations of the theory and 1-cell constructors to impose the axioms.
However, a theorem of Andreas Blass says that (assuming the consistency of some large cardinals) ZF does not construct free algebras for all algebraic theories (the paper is called Words, free algebras, and coequalizers). The idea is that if you had free algebras then you could build well-orderings of arbitrarily high cofinality, and therefore arbitrarily large regular cardinals; but a theorem of Gitik says that ZF is consistent with all uncountable cardinals being singular.
It seems likely that a principle much weaker than full AC could be added to ZF to enable the construction of 1-HITs, however. Some related discussion is here.
This is a very good step forward from a technical point of view: it should really simplify the proof-theory of HITs by reducing everything to just the usual type theory plus 1-HITs. The real boost in expressive power comes from the combination with dependent types: a disc is an interval with one end in motion over a lower-dimensional sphere, i.e. parametrized as a dependent type.
It’s also very neat how the logical and homotopical ideas fit together: we have the similar reduction of higher to lower dimension using suspensions, and this gives a formalization and generalization of that in logical terms.
To avoid any possible confusion, maybe it’s worth stating explicitly that this does not mean that all higher dimensional types are really just 1-dimensional — i.e., that there are no types properly above h-level 3. An n-HIT specified in this way as an elaborate combination of parametrized 1-HITs will still in general have h-level n, even for large n. The reduction is not on the side of “what there is”, but just of how we describe it.
Indeed — in fact, an n-HIT (however specified) can even have h-level higher (or lower) than n. The 2-HIT
has (at least in classical homotopy theory — we haven’t proven this in HoTT yet) no finite h-level.
yup.