Back in the summer of 2012, emboldened by how nicely the calculation π₁(S¹) had gone, I asked a summer research intern, Joseph Lee, to work on formalizing a proof that the higher-inductive definition of the torus (see Section 6.6 of the HoTT book) is equivalent to a product of two circles. This seemed to me like it should be a simple exercise: define the functions back and forth by recursion, and then prove that they’re mutually inverse by induction. Joseph and I managed to define the two functions, but after spending a while staring at pages-long path algebra goals in both Agda and Coq, we eventually threw in the towel on proving that they were mutually inverse. By the end of the IAS year, both Kristina Sojakova and Peter Lumsdaine had given proof sketches, and Kristina’s later appeared as a 25-page proof in the exercise solutions of the book. But it still bothered me that we didn’t have a simple proof of what seemed like it should be a simple theorem…
Since the Bezem, Coquand, and Huber cubical sets model of HoTT was developed, Guillaume Brunerie and I have been thinking about cubical type theories based on these ideas (more on that in some other post). As part of this, we have also played with using cubical ideas in “book HoTT” (MLTT with axioms for univalence and HITs) in Agda. The main ingredient is to make use of more general “cube types” than just the identity type (the special case of lines). Each cube type is dependent on the boundary of a cube, and represents the “inside” of the boundary. For example, we have a type of squares, dependent on four points and four paths that make up the boundary of a square. And a type of cubes, dependent on the eight points, twelve lines, and six squares that make up the boundary of a cube (implicit arguments are crucial here: everything but the squares can be implicit). Another ingredient is to use path-over-a-path and higher cube-over-a-cube types to represent paths in fibrations.
Now, these cube types are not really “new”, in the sense that they can be defined in terms of higher identity types. For example, a square can be represented by a disc between composites, and a path-over can be reduced to homogeneous paths using transport. However, isolating these cubes and cube-overs as abstractions, and developing some facts about them, has allowed for the formalization of some new examples. Guillaume used this approach to prove the 3×3 lemma about pushouts that is used in the calculation of the Hopf fibration. I used it to resolve a question about the contractibility of a patch theory. Evan Cavallo used it in the proof of the Mayer-Vietoris theorem.
And, we finally have a simple write-the-maps-back-and-forth-and-then-induct-and-beta-reduce proof that the torus is a product of two circles.
You can read about it here:
A Cubical Approach to Synthetic Homotopy Theory
Daniel R. Licata and Guillaume Brunerie
Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe higher-dimensional paths. While some aspects of homotopy theory have been developed synthetically and formalized in proof assistants, some seemingly straightforward examples have proved difficult because the required manipulations of paths becomes complicated. In this paper, we describe a cubical approach to developing homotopy theory within type theory. The identity type is complemented with higher-dimensional cube types, such as a type of squares, dependent on four points and four lines, and a type of three-dimensional cubes, dependent on the boundary of a cube. Path-over-a-path types and higher generalizations are used to describe cubes in a fibration over a cube in the base. These higher-dimensional cube and path-over types can be defined from the usual identity type, but isolating them as independent conceptual abstractions has allowed for the formalization of some previously difficult examples.
Homotopy Type Theory 
Impression of the whole actual note: an instance of Ronnie Brown’s frequent contention?
Yes, I had that thought too! The entire double-categorical community should also be happy. Not only do we have double and also triple-categorical operations going on, but “whisker-square” looks like one of the operations in Verity’s “double bicategories”.
This is very nice! It will take me some time to digest it. I wish I had some time right now to experiment with square and cube types in Coq. Maybe someone else will pick it up. A few questions to start with:
So is your conclusion that it’s more convenient to give things like dependent paths and square types their own inductive definitions, rather than defining them in terms of existing globular path operations and transport? I’ve shied away from that because then operations like your hom-to-over/left-eqv are not judgmental. I think you said that if we define PathOver using transport, then it would still satisfy the same induction principle and computation law; is the main reason to prefer an inductive definition the fact that Agda has pattern-matching syntax for inductive definitions?
How much of the convenience of square-types for the torus proof has to do with the fact that squares and cubes arise from dependent paths over paths, and how much has to do with the fact that the 2D path constructor of the torus is a square? In particular, when we start working with more general cell complexes, will squares and cubes still be enough, or should we expect to also need triangles, pentagons, etc. etc.? (I see that in the
lemma there is already an octagon quietly hiding…)
Have you tried abstracting from the proof of t2c2t a general “
-rule” for functions out of the torus? I.e. given two functions 
, what hypotheses about the behaviour of 
on the constructors enable us to conclude 
? This ought to enable proving the universal property of the torus, which might lead to another, less direct, proof of the equivalence with 
.
Thanks for the questions, Mike! Answering in reverse order: I just did the universal mapping property for the torus here: https://github.com/dlicata335/hott-agda/blob/master/lib/spaces/Torus.agda
Overall, we get an Equiv (T → X) (T-rec-prem X) where T-rec-prem X is
Σ (a : X). Σ (pq : Path a a × Path a a).Square (fst pq) (snd pq) (snd pq) (fst pq) and the maps are (right-to-left) the recursor T-rec and (left-to-right) applying to each constructor. The two composites are a “beta” direction, which says that applying T-rec a’ p’ q’ f’ to the constructors gives (a’, p’, q’, f’) and an “eta” direction, which says that g : T -> X is the same as T-rec (g a) (ap g p) (ap g q) (ap-square g f). From this you get that f,g : T -> X equal if applying them to constructors is the same in T-rec-prem X, and you could expand out what equality in that Sigma means if you wanted.
Great! Now you or someone else who speaks the cube library can try using the UMP to prove the equivalence with
. (-:
I remember trying this (by postulating the UMP, which we can now prove from the dependent elim) during the IAS year at your suggestion. I think it wouldn’t be hard to get the equivalence {X} (S1 * S1 -> X) = (T -> X), but then what’s the final yoneda-y step? You calculate that the forward direction of the above equivalence is the same as post-composition with the t2c : T->S1*S1 function, and then what? Somehow that tells you that t2c is an equivalence, right?
Here’s the best lemma I could come up with:
{A B : Type} (f : B → A) (e : {X : Type} → (A → X) ≃ (B → X)) (pc : {X : Type} (g : A → X) → coe e g == g o f) (eqvi : IsEquiv (coe e (\ x -> x))) where -> IsEquiv fI.e. to show that f is an equivalence, you can show that maps from A->X are the same as maps from B->X, show that this equivalence is post-composition with f, and show that coercing the identity along e is an equivalence.
But are both of those hypotheses necessary, or does eqvi follow for general reasons? I don’t remember thinking that I needed to prove that last time.
Yes. Given e : forall X, (S1 * S1 -> X) (T -> X) whose forward direction is precomposition with t2c, define c2t to be (e T)^-1 idmap. Then c2t o t2c is e T (e T)^-1 idmap which is idmap. For the other direction, first prove that (e X)^-1 f = f o (e X)^-1 idmap by moving (e X)^-1 from left to right and using associativity of composition. Then t2c o c2t = (e T)^-1 t2c which is the identity since t2c = e T idmap.
got it, thanks!
Even for HITs with only path constructors, squares seem like they come up fairly often, because whenever you prove (x : HIT) -> f x == g x by induction, you get a path-over in a path type. And even if you only have 1-constructors, writing a binary function by nested induction (S1 -> S1 -> X), or nesting the HIT (pushout of pushouts) seems to boost the dimension. So it’s not just the face constructor.
I don’t really have a sense for what would happen with other cell complexes. Because of the definitional equalities on refl, I would guess that viewing triangles as degenerate squares might not be too painful. But if you have more than four lines, you’d have to make some arbitrary choices again, and I’m not sure what would happen.. Is there a good first test example along these lines to look at?
Maybe the genus 2 surface as an octagon (see picture here: https://math.stackexchange.com/questions/479371/constructing-a-genus-2-surface-from-8-gon) would be a good example?
In general, you can make genus g surface from a 4g-gon.
What would we prove about it?
Well, we could calculate its fundamental group to start with.
Besides the fundamental group, I was also thinking of homology and Euler characteristic.
The fundamental group is some funny quotient, right? Can we say Euler characteristic in HoTT?
π1 ~~ ; in case it helps (e.g. for an encoding-decoding machine), this group is word-hyperbolic.
gyah; why should a fellow forget what tags mean?
Yes, the fundamental group should be generated by four elements
subject to something like 
.
Off the top of my head, I can think of two potential ways to say Euler characteristing in HoTT: (1) the alternating sums of the ranks of the (co)homology groups and (2) the trace of the identity map of the suspension spectrum. I think the second will almost certainly work, but will require a lot of intermediate definitions like the smash product of spectra. The first is a little questionable in general since “rank” may be hard to define constructively, but at least for small concrete spaces like these it may work.
That makes sense. The octagon might be worth a try, but it might also not be worth the trouble. I kind of doubt that we’ll ever really want to be writing out concrete particular cell complexes that are very much more complicate than the torus, rather than manipulating them at some higher level of abstraction. But I could be wrong.
In Agda, there are two things that make the primitive inductive families convenient: (1) Doing e.g. square induction by pattern matching on the square, as opposed to many pattern matches on the sides and then the disc. This was convenient for *writing* the library, but I’m not yet sure how often you’ll do square induction in client code. So while it made my life easier, maybe it was the wrong choice, because otherwise you could have one of the equivalences with the other definitions be definitional. (2) Unification in Agda is up to definitional equality, so Agda won’t fill in implicit arguments in positions that reduce. So if we defined Square p id id q = p == q then some of the uses of implicit arguments might not work? I haven’t actually tested this, but that’s why I did it that way. I think Evan Cavallo did a non-inductive-family definition when he ported some of these ideas to HoTT-Agda, so maybe he can comment. Of course, you could avoid using an inductive family and define Square p q r s as an inductive type with one constructor that wraps a disc to get around this.
In Coq, I don’t think these issues are relevant, because for (1) you could just prove and then apply square induction in tactics as conveniently as if it were the primitive elimination form (unlike Agda, where you often have to write out the induction formula if you use an eliminator) and for (2) Coq unification is not up to definitional equality, right? So I don’t think it would make much of a difference which definition you take.
More later, but quickly: what does it mean for unification to (not) be up to definitional equality? Do you mean that Coq might fail to unify two terms that are judgmentally equal but not syntactically equal, whereas Agda’s unification will always detect judgmentally equal terms?
Sorry, I didn’t make the right distinction there. What I meant was that Agda unification only succeeds when the result is unique up to definitional equality, whereas I think Coq is willing to proceed with a unifier even if it isn’t unique up to definitional equality. So when you have a unification constraint like “f ? = f 0” and f pattern-matches on its argument, Agda will not necessarily succeed with ? = 0, because maybe f 7 reduces to 0 too, so up to definitional equality ?=0 is not unique. There is some injectivity analysis in Agda, so sometimes it does get this. I think Coq will always/sometimes get this. So sometimes Agda has trouble with positions that you pattern-match on. On the other hand, if Square is defined as a datatype, then Square is treated as injective.
Okay, thanks. That’s at the level of things about type theory that I don’t quite understand yet, but it makes a little sense.
Regarding your point (1), I think there could still be some value in Coq to having a primitive elimination. For instance, match statements, the closest analogue of Agda’s pattern-matching, only work on actual inductive datatypes; it’s just that they’re used explicitly less frequently because of tactics. Moreover, the standard tactics like destruct and induction will also, as far as I know, only work on actual inductive datatypes; destruct actually inserts a match statement into the proof term, while induction calls the eliminator but its list of things that count as “eliminators” is populated automatically when you make inductive definitions. So you’d have to say apply square_ind or refine (square_ind _ _ _ ...). Of course, that’s what we do all the time with HITs.
I would think that one could write a tactic that applied a derived square_ind in the same way that it would apply a primitive one, so you’d just have to say my_destruct or my_induction or something.
Yes, probably. Jason could probably write a better such tactic than I could. (-:
On the other hand, in Coq one could also do the “many pattern matches” directly with a single path_induction tactic invocation.