add functoriality lemmas for pushout

[Alizter]

I've proven these lemmas many times before, but never managed to push them. Here is a fresh attempt.

[jdchristensen]

I wonder if these would be easier to prove if functor_pushout was defined using Pushout_rec? For example, the proof of functor_coeq_beta_cglue is a one-liner, so maybe the same would be true here?

[Alizter]

I wonder if these would be easier to prove if functor_pushout was defined using Pushout_rec? For example, the proof of functor_coeq_beta_cglue is a one-liner, so maybe the same would be true here?

They are a little harder to prove using Pushout_rec directly. Here is a proof I had laying around from before:

+  Definition functor_pushout_compose
+    {A B C f g A' B' C' f' g' A'' B'' C'' f'' g''}
+    (u : A -> A') (v : B -> B') (w : C -> C')
+    (u' : A' -> A'') (v' : B' -> B'') (w' : C' -> C'')
+    (p : v o f == f' o u) (q : w o g == g' o u)
+    (p' : v' o f' == f'' o u') (q' : w' o g' == g'' o u')
+    : functor_pushout (u' o u) (v' o v) (w' o w)
+        (comm_square_comp' p p') (comm_square_comp' q q')
+      == (functor_pushout u' v' w' p' q') o (functor_pushout u v w p q).
+  Proof.
+    serapply Pushout_ind_dp.
+    1,2: reflexivity.
+    intro a; cbn.
+    apply sq_dp^-1, sq_1G.
+    symmetry.
+    refine (ap_compose (functor_pushout u v w p q) _ (pglue a) @ _).
+    rewrite Pushout_rec_beta_pglue.
+    rewrite 2 ap_pp.
+    unfold comm_square_comp'.
+    rewrite <- 2 ap_compose.
+    rewrite 2 Pushout_rec_beta_pglue.
+    rewrite ?ap_V.
+    rewrite ?ap_pp.
+    rewrite <- ?ap_compose.
+    unfold functor_pushout.
+    by rewrite ?concat_pp_p, inv_pp.
+  Defined.

You can ignore the dp stuff, but you can see but there are a lot of ap_compose and ap_pp. For something like functor_join this approach is better, but functor_pushout has these annoying paths on the end which make managing them cumbersome.

[jdchristensen]

Well, that looks similar, since the current proof does things 2 steps at a time. (Also note that the Coeq result is Qed.) But I think it would improve if functor_pushout was defined directly using Pushout_rec, as shown below. And note that functor_pushout_beta_pglue becomes a one-liner:

Definition functor_pushout
  {A B C} {f : A -> B} {g : A -> C}
  {A' B' C'} {f' : A' -> B'} {g' : A' -> C'}
  (h : A -> A') (k : B -> B') (l : C -> C')
  (p : k o f == f' o h) (q : l o g == g' o h)
  : Pushout f g -> Pushout f' g'.
Proof.
  snrapply Pushout_rec.
  - exact (pushl o k).
  - exact (pushr o l).
  - intro a.
    exact (ap pushl (p a) @ pglue (h a) @ ap pushr (q a)^).
Defined.

Definition functor_pushout_beta_pglue
  {A B C} {f : A -> B} {g : A -> C}
  {A' B' C'} {f' : A' -> B'} {g' : A' -> C'}
  {h : A -> A'} {k : B -> B'} {l : C -> C'}
  {p : k o f == f' o h} {q : l o g == g' o h}
  (a : A)
  : ap (functor_pushout h k l p q) (pglue a)
    = ap pushl (p a) @ pglue (h a) @ ap pushr (q a)^
  := Pushout_rec_beta_pglue _ _ _ _ _.

So I think this is another case where trying to reduce to Coeq rather than using the custom recursion and induction principles is going to make things a bit harder.

[Alizter]

I've managed to change functor_pushout to use Pushout_rec instead. This was tricky to do but still possible, I had to change some place in ReflectiveSubuniverses that required that specific definition by introducing an appropriate lemma.

[Alizter]

Actually, I didn't manage to fix everything whoops.

[jdchristensen]

Oh, I had no idea that various things depended on defining functor_pushout in terms of functor_coeq. Do you think things were better off before you implemented my suggestion or as they are now? Even the new functoriality results were a fair bit of work.

[jdchristensen]

In particular, I'm surprised by how complicated functor_pushout_homotopic is. I wonder if some lemmas would help with a lot of the repeated things. For example, in this PR (still WIP) we added Colimit_rec_homotopy and Colimit_rec_homotopy', which simplified arguments about functor_Colimit.

[jdchristensen]

@Alizter Any thoughts on my two previous comments?

[Alizter]

Sorry I seem to recall writing a reply before, but it looks like I never sent it. I think we should revert to before the functor_pushout change since proving it from pushout_rec didn't really have any advantage.

It might be possible to write down some lemmas, but it isn't obvious to me if that would improve anything.

[jdchristensen]

Ok, feel free to revert to before my suggestion (maybe by force pushing to keep the history clean).

About the additional lemmas, Colimit_rec_homotopy and Colimit_rec_homotopy' allow you to avoid the idiom where you: "apply rec, apply transport_paths, apply betaglue" by encapsulating them in a lemma. I see a lot of those steps in the current version that would disappear, but I don't recall if they also happened in the previous version.

(It would be nice if all of our specific colimit files had the same pattern of results and helper lemmas...)