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
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.