Blakers-Massey

[Alizter]

Having GBMT in the library would be a massive benefit. It would allow us to prove Freudenthal. There are currently two proofs that I know of in arXiv:1605.03227.

Which one would be better to formalise?

And roughly what would need to be done in order to formalise it. I am guessing this will not be very easy to write.

[mikeshulman]

I think the "type-theoretic" proof would probably be better to formalize. I would probably start by defining the "pushout of a dependent span" taking as input R : A -> B -> Type in terms of our pushouts of functions, and deriving its induction principle from those. Then start following the proof as written in the paper, except that instead of the "wedge connectivity lemma" you would use the hypothesis that a certain join is modal for some modality.

I started messing around at https://github.com/mikeshulman/HoTT/blob/blakers-massey/theories/Homotopy/BlakersMassey.v, and got up through constructing the maps in either direction for the path case of the definition of code. I haven't looked at the original Agda formalization (and I have a hard time reading Agda anyway); one could either attack this by doing explicit transports and path algebra or by trying to hit everything with J. I started doing the former at first, but then the latter started to seem easier so I switched. However it could bite later. Feel free to have a go pushing it forward if you like; I really shouldn't spend any more time on this. But I thought it might be helpful to at least set up the definitions and hypothesis the way I think they should go.

[mikeshulman]

It might also be worth looking at the ABFJ paper to see whether their proof would become something slicker if translated back from oo-categories into HoTT. That's happened before.

[Alizter]

I had a look at your formalisation, and I made some tiny progress here and there (your second path lemma is quite easy to prove by destructing the paths). It is quite difficult to work on overall however due to all the matches that have to be made. I am guessing there is some cleaner way of doing what has been done, that will reduce clutter.

I have been reading ABFJ in detail and I am beginning to like what I see. As far as I can tell this is a much nicer proof than setting up an encode-decode. I don't know any oo-topos theory so I am learning as I go here. I am a bit confused with the arrow topos and what that means for HoTT, an example is Lemma 4.2.2, I am guessing that this is a family of equivalences but I am not so sure. I don't see anything that is too problematic, I will need to think a bit more about descent however.

Also thank you for having a go at this! I know you are extremely busy at the moment so you have my gratitude. :-)

[Alizter]

Ok so I have a commutative square g o a1 == a2 o f with f : A -> B and g : C -> D and I want to "factorise" this using some modality. In Factorization.v there is such a diagram at around line 300. I need to use the q that is defined there since this gives me two commutative squares q1 and q2. How can I access these?

I am guessing I need to change the Lets to Definition however is this the best way?

It seems that the ABFJ paper can prove the GBMT using arguments about modalities.

---

Edit: Here is my formalisation if you want to play with it.

[mikeshulman]

Of course they use arguments about modalities; the theorem is about modalities.

Yes, I think if you want to access that q explicitly you should change it to a Definition, and give it a more descriptive and globally-unique name at the same time.

[Alizter]

Actually after reading it a bit more I think this is lemma 1.44 in the modalities paper which isn't really what I want at all.

On page 11 of the ABFJ paper there is a diagram at the bottom. I cannot figure out how the map between intermediate objects is constructed. I think there are a few typos in the diagram too.

[mikeshulman]

Are you looking at v2 of the paper instead of v3? In v3 I think the diagram you mean is on page 12. And I do think that intermediate morphism is q.

[Alizter]

@mikeshulman However to access q I am required to show that a1 is connected and a2 is truncated, however there is no such restriction in the paper. What has been formalised is that q is an equivalence when those conditions hold so I suppose I need to get rid of them somehow.

It seems my printed copy of the paper is v2 like you've said.

[mikeshulman]

Oh, sorry, I missed that. Okay I guess it's not exactly q. The intermediate map in this case comes from the lifting property (lift_factsys in Factorization) applied to L(f) and R(g).

[Alizter]

@mikeshulman I am currently playing around with your start at BM. I don't know if you are aware, but you don't need those big change statements, since you can do the following:

            change x0 with xq.1.
            change q00 with xq.2.
            change y1 with yq.1.
            change q11 with yq.2.

This might make it easier to work with.

[Alizter]

This lemma is not so easy to prove it seems.

Definition foo {A : Type} {x y : A} (p q : x = y) (r : p @ p^ = q @ p^)
  : moveR_1M _ _ ((concat_pV p)^ @ r)
    = cancelR p q p^ r.

No matter what I destruct, I always end up with a goal like 1 = r. I am starting to doubt that this is even true...

[mikeshulman]

That is a tricky one. Part of the problem is that lemmas like moveR_1M were not designed to be reasoned about. Here's the first proof I came up with; it could probably be improved:

Definition moveR_1M_compute
           (A : Type) (x y : A) (p q : x = y) (r : 1 = q @ p^)
  : moveR_1M p q r = (concat_1p p)^ @ moveR_pM p q 1 r.
Proof.
  destruct p; cbn.
  rewrite concat_p_pp; apply whiskerR.
  rewrite !concat_1p; reflexivity.
Qed.

Definition moveR_pM_nat
           (A : Type) (x y z : A) (p : x = z) (q : y = z) 
           (r r' : y = x) (s : r = r') (h : r' = q @ p^)
  : moveR_pM p q r (s @ h)
    = whiskerR s p @ moveR_pM p q r' h.
Proof.
  destruct s; cbn.
  rewrite !concat_1p; reflexivity.
Qed.

Definition moveR_pM_compute (A : Type) (x y z : A) (p : x = z) (q : y = z) 
           (r : y = x) (s : r = q @ p^)
  : moveR_pM p q r s = 
    ((whiskerL r (inv_V p))^ @ whiskerR s (p^)^ @ concat_pp_V q p^).
Proof.
  destruct p, q; cbn in *.
  rewrite ((inv_V s)^).
  set (s' := s^); clearbody s'; clear s.
  destruct s'; reflexivity.
Qed.

Definition foo {A : Type} {x y : A} (p q : x = y)
           (r : p @ p^ = q @ p^)
  : moveR_1M _ _ ((concat_pV p)^ @ r)
    = cancelR p q p^ r.
Proof.
  transparent assert (t : (p = q)).
  { refine ((concat_p1 _)^ @ _).
    refine ((whiskerL p (concat_Vp p)^) @ _).
    refine (concat_p_pp _ _ _ @ _).
    apply moveR_pM.
    exact r. }
  transitivity t; subst t.
  - rewrite moveR_1M_compute.
    rewrite moveR_pM_nat.
    rewrite !concat_p_pp.
    apply whiskerR.
    destruct p; reflexivity.
  - unfold cancelR.
    rewrite moveR_pM_compute.
    rewrite !concat_p_pp.
    apply whiskerR.
    apply whiskerR.
    destruct p; reflexivity.
Qed.

The _compute lemmas could presumably be eliminated by defining the moveR lemmas to be their RHSs, making them true by definition (I haven't tried to see whether this would break anything else in the library, but I'd be very surprised if it did). Note that cancelR is already defined in terms of other things, so we can just unfold it.

[Alizter]

@mikeshulman So I defined moveR as you said. It only broke the lemma isequiv_moveR_1M in Types.Paths but interestingly typeclass search was able to prove it. So this definition seems to make that proof shorter too. The rest of the library is fine. It might be worth redefining all the moves.

[mikeshulman]

Feel free!

[Alizter]

Have you got any suggestions on proving the sections? I've managed to move things around with O_rec_poscompose but I can't see anything that will reduce down.

[mikeshulman]

No, I don't have time to think about this any more. If you're stuck, you could go back to the original Agda formalization and copy their approach.

[mikeshulman]

Thanks for pointing out change ... with ... by the way; i'll try to remember that next time.

[Alizter]

Now that #1078 has been merged, we can close this.