Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
3x3 lemma for pushouts
There are many constructions such as joins, which would benefit greatly from having this lemma. It is described in Brunerie's thesis, apparently suggested by Finster.
On my 3x3 branch I have added the 3x3 lemma.
Currently I have tried clawing at some path algebra, however I didn't really have a technique in mind and essentially have been trying random rewrites until I can beta reduce all the pps. It is getting difficult to work with since coq has become very slow.
The proof is long and tedious but would be tremendously useful if it can be finished. For starters we can prove associativity of join. So I am asking for help on what to do.
I think what needs to be done is to prove some more lemmas that will reduce some of the long path algebra. I think this is what Brunerie did in his agda formalisation but I can't read it very well.
I am guessing I have really only completed around 5% of the proof. It may also be in our interests to move it out of Pushout.v so that it doesn't slow down compilation.
(In case anyone watching is confused, this is about the 3x3 lemma for pushouts -- the 3x3 lemma for pullbacks is in Fibrations.v.) This is a notoriously difficult lemma to prove; I don't know anything about how Brunerie did it. Is it done in Lean? My first instinct as a category theorist would be to use the Yoneda lemma and compare universal properties, transforming the theorem into one about pullbacks which are often easier to reason about, but I don't know whether that would help. I would definitely agree with moving it into its own file, but I don't have any other suggestions offhand other than that "trying random rewrites" is unlikely to work without a more structured approach of some kind. (-:
So the agda-formalisation has a whole folder for this lemma. Floris seems to have written it down in the spectral library, but nothing has been attempted there. The lean and coq proofs ought to look very similar.
So I have spoken with Brunerie and he says the best way to go about it is to use cubical stuff. I have gone ahead and merged Mike's cubical branch into 3x3 and added a few more lemmas to Square.v including Kan fillings. Using it in the proof seems much more manageable but I am still stuck in pretty much the same place it would seem (at least I can see it more clearly).
The new link is: https://github.com/Alizter/HoTT/blob/3x3/contrib/3x3Pushout.v
I will have to think about this some more.
So quick update. I have managed to finish the to and from functions for the equivalence. The big help was packaging things up in cubical abstraction. In order to give the sections of the equivalence I will need to write a new pushout_ind that takes a square rather than a transport and has its own beta reduce etc. This will allow me to work directly with cubes.
Due to the number of rewrites I am using, the definitions of to and from are getting very unwieldy, so I can't hope to expand them and simply reduce everything out.
I'm happy to hear you're making progress! In general it doesn't work very well to use rewrite when constructing things that you're going to have to reason about later on, though.
What's the alternative to rewriting? I have never really understood how coq rewrites subterms. I understand that it is using paths_ind but I don't understand how it can do that to a subterm.
Instead of rewriting you can manually apply all the necessary aps and transports to turn a path between subterms into a path between the whole terms. E.g. if you have P (p @ 1) then instead of rewrite concat_p1 you can say something like refine (transport P (concat_p1 _)^ _).
I have rewritten to and from using refines now. I could probably improve the speed by hinting to coq a bit more but it is reasonable for now.
It is not easy to reason about, coq is really struggling with the length of the goal, especially if I unfold it. I have no clue how to make this any easier.
Well, without having looked at it, a standard trick is to find lemmas that you can prove in isolation and then apply in the main theorem rather than doing it all at once.
Here's a random thought that just occurred to me. A 3x3 diagram should be equivalently representable in a "dependently typed" form:
A00 A10 A01 A11 : Type
A0x : A00 -> A01 -> Type
A1x : A10 -> A11 -> Type
Ax0 : A00 -> A10 -> Type
Ax1 : A01 -> A11 -> Type
Axx : forall (a00 : A00) (a01 : A01) (a10 : A10) (a11 : A11),
A0x a00 a01 -> A1x a10 a11 -> Ax0 a00 a10 -> Ax1 a01 a11 -> Type
and this makes all the squares therein commute judgmentally. Moreover, such a dependently typed 3x3 diagram naturally has a "symmetric double pushout" defined cubically with four point constructors, four path constructors, and one square constructor. Is there any chance it might be easier to start with a diagram of this form and show that its two iterated pushouts are equivalent to the symmetric one, hence equivalent to each other?
How do we get the 3x3 diagram back from the "dependently typed form"? I don't see how the maps are encoded.
The maps are projections from sigma-types. The corner objects are A00, A01, A10, and A11. The object on one side is { a00 : A00 & { a01 : A01 & A0x a00 a01 } }, and its two maps to the corners are pr1 and pr1 o pr2. And so on.
Ok so I can see how we get 9 objects and 12 maps from this. How do we turn 9 objects and 12 maps into this dependently encoded type however?
The same way you turn any map into a dependent family over its codomain:
A0x a00 a01 = { x : A0x' & (f0x0 x = a00 * f0x1 x = a01) }
OK so I have played around with this in coq, I am a bit stuck trying to make Axx however. See my Dep3x3 branch.
Edit: actually nevermind, I managed to work it out.
@mikeshulman I am having a look at this again. Can you elaborate on your "symmetric double pushout" and what you expect it to look like?
Sorry, Mike there was nothing unclear. Andreas and I are currently working on it. We have sort-of managed to define the HIT.
What happens to square constructors in the dependent eliminator? I had to make some sort of dependent path between Dependent squares. Is this some sort of dependent cube, because I don't see it?
I think the way to deal with square constructors is described fairly clearly in http://dlicata.web.wesleyan.edu/pubs/lb15cubicalsynth/lb15cubicalsynth.pdf.
I stopped working on this about a month ago, since the path-algebra (even with the cubical library) got a bit heavy. I am sure if I drank enough coffee I could get through it but it is an exhausting proof. I might however be hindering myself somehow but I am unsure.
Egbert sketched to me the proof he wants to use in his notes which I think is exactly what Mike said at the top. The idea is that if X is a pushout, then equivalently forall Z, Z^X is a pullback. The 3x3 lemma for pullbacks is a lot simpler to prove, since it can be shown that pullbacks preserve sigmas and paths, hence pullbacks.
Of course there is some work getting the exponential to work with the diagram, but this looks promising. :-)
Another argument has come to mind. Colimits satisfy the property of "having a right adjoint". From this we can show that the colimit functor preserves colimits. Hence colimits commute. From this it ought to be possible to show that pushouts commute with pushouts. This approach feels promising, I will see if it works.
OK, I have made some progress. Egbert's suggestion does work. I have managed to formalize a (terribly written) proof that (R -> X) <~> (C -> X) for all X, where R is the pushout of the rows and C the pushout of the coloumns. Obviously using yoneda, R <~> C when the equivalence is natural in X.
I hope that natuarlity won't be too difficult, I think it will follow from reduction. For me to do this however, I need to fully finish the equivalence (R -> X) <~> (C -> X) the only thing left to do is the 3x3 lemma for pullbacks.
Great! One of my hopes with wild categories was that an equivalence such as this could be constructed in an evidently natural way by chaining together known natural equivalences.
I agree with Mike. We should be able to show that wild left adjoints preserve wild colimits, and show that the functor taking a diagram to its colimit is itself a wild left adjoint. That should prove the 3x3 lemma for pushouts. Wild category theory would be a great theory to organize all the relevant lemmas and constructions.
However, I am still happy that this approach now seems to work in Coq.
