functoriality of smash

[Alizter]

Here is a new attempt at the functoriality of smash. I've done it directly without using the swapping infrastructure in the Hurewicz formalization. It was quite straightforward and allowed me to define some useful lemmas about ap011. (Actually from what I could tell, this wasn't proven to the full extent in the Hurewicz formalization anyway).

I'll wait till after #1886 which will mean some proofs will need to be shifted around.

[jdchristensen]

It's great to have this!

A few of the Defined lines are a bit slow. Not sure if that is because of the simpl + pelim, or because of the long proofs.

Many of the proofs follow the same pattern. Is there a lemma that can be written to handle the boilerplate? That would make it easier to read and might speed up the Defined lines.

Also, the proofs have symmetrical path algebra. It would be nice if that could be handled using swap instead of being duplicated, but that could be considered for a future PR.

[jdchristensen]

Oh, about naming, I think we most often use names like functor_join, functor_sigma, functor_coeq, etc. (Exceptions are Trunc_functor and O_functor.) I like the functor_* naming, since it also meshes with is1functor_*, etc.

[jdchristensen]

About a lemma for handling the boilerplate, I'm thinking of something like bundle_joinrecpath in Join/Core.v. This specifically handles proving that that two functions defined using join_rec with definitionally equal point constructors are homotopic and I was able to use it in many situations. However, most of the lemmas you need to prove aren't exactly of this form, so maybe it's not quite the right abstraction.

[Alizter]

Thanks for taking a look. I'm not yet certain what the boiler plate code should look like. When proving symmetry and associativity, they started requiring a lot of non-trivial paths so it is not that common outside of functionality it seems.

[jdchristensen]

I think all of the new proofs would benefit from pointed_reduce.

About the boilerplate, I mean how every proof uses Build_pHomotopy, Smash_ind, reflexivity for the 2nd and 3rd goals, and transport_paths_FlFr' for the 4th and 5th goals. Something like Join_ind_FlFr is maybe the best model, with auxl and auxr assumed to be going to the same points.

I also wonder if such a lemma could require a swapped version of the 5th goal, so that exactly the same tactics might be used to prove the 4th and 5th goals.

[Alizter]

I tried to understand how to simplify the proof of functor_smash_homotopic using pointed_reduce but I didn't get very far. Overall it doesn't seem to help much there. Could you take a look too?

[Alizter]

I've pushed my attempt which does some simplificiation, but most of the proof is the same.

[jdchristensen]

You need to do pointed_reduce with everything in the context, and without manually destructing anything. The following works and is shorter than your proof:

  pointed_reduce.
  snrapply Build_pHomotopy.
  { snrapply Smash_ind.
    - intros x y; simpl.
      exact (ap011 _ (p x) (q y)).
    - reflexivity.
    - reflexivity.
    - intros x.
      nrapply transport_paths_FlFr'; simpl.
      lhs nrapply concat_p1.
      lhs nrapply Smash_rec_beta_gluel.
      rhs nrapply whiskerL.
      2: nrapply Smash_rec_beta_gluel.
      induction (p x); simpl.
      rhs_V nrapply concat_pp_p.
      apply whiskerR.
      nrapply ap_pp.
    - intros y.
      nrapply transport_paths_FlFr'; simpl.
      lhs nrapply concat_p1.
      lhs nrapply Smash_rec_beta_gluer.
      rhs nrapply whiskerL.
      2: nrapply Smash_rec_beta_gluer.
      induction (q y); simpl.
      rhs_V nrapply concat_pp_p.
      apply whiskerR.
      nrapply (ap011_pp _ _ _ 1 1). }
  symmetry; simpl.
  lhs nrapply concat_p1.
  apply ap022; apply concat_p1.

But unfortunately the Defined line is a lot slower. Maybe the slowness can be fixed? Or maybe just the idea of doing induction (p x) can simplify your proof, without the pointed_reduce? Also, there's a general lemma that comes up in yours that could be abstracted out (or maybe it is in PathGroupoids already)? For f : A -> B, p : forall a, f a = b, q : a0 = a1, we have ap f q @ p a1 = p a2. In another spot, you could use ap011_is_ap', with the order reversed, to simplify things.

[Alizter]

@jdchristensen I wanted to mention that I also pushed an easy proof of symmetry for smash products here too after doing the simplifications you suggested. I also quickly remembered why associativity was problematic. Hopefully, we can eventually experiment with some of Axel's insights into the problem.

One thing that has been bothering me is that the "recursion data" for smash products seems to use funext in an essential way, whereby you need funext to show A ->* (B ->** C) is pointed. Have you got any ideas if funext can be removed here? If so, then I think we can also make some progress on funext-free associativity a.la. van Doorn by doing the ZeroGroupoid dance.

[jdchristensen]

One thing that has been bothering me is that the "recursion data" for smash products seems to use funext in an essential way, whereby you need funext to show A ->* (B ->** C) is pointed.

Well, I guess that's not the right way to express the recursion data. It should consist of the constructors of the smash product expressed in C, just like the arguments of Smash_rec.

(BTW, I see that Smash_rec' takes two arguments ql and qr that are not needed.)

[jdchristensen]

after doing the simplifications you suggested

I wasn't happy with how slow the Defined was with those changes, so I was hoping for a different way... I had some suggestions above, but I'd also be ok with some rewrites, as they sometimes make proofs both shorter and faster...

[Alizter]

I've used the new bifunctor constructors to define the smash functor. The definition is now much cleaner. I see the slowdown you are talking about @jdchristensen, however I haven't got any ideas how to speed it up.

[jdchristensen]

I can't figure out what has changed. I know that sometimes forced pushes are needed (e.g. this was probably a rebase), but when possible it's better to add commits. E.g. when I have your branch checked out, it makes it much easier to update it and see exactly what changed. And even through the github interface, it's much easier to navigate.

As far as I can tell, there are several comments that could be addressed:

• The proof of functor_smash_homotopic that I suggested causes a slow Defined.
• pointed_reduce can probably simplify other proofs.
• A general lemma like Join_ind_FlFr could probably eliminate a lot of boilerplate (and maybe will speed things up?)
• Can we use symmetry to avoid having to duplicate proofs with symmetrical proofs?

[Alizter]

@jdchristensen Sorry about that. I will try to avoid force pushing from now on. FTR I have not modified any commits during each force push and only added commits after each review suggestion / modification. Your suggestion for the proof of functor_smash_homotpic is the commit with description improve proof of functor_smash_homotopic for instance.

[Alizter]

I'll try and address the other points you brought up later when I get some time.

[Alizter]

@jdchristensen

• I haven't been able to speed up the proof of functor_smash_homotopic. It currently finishes the Defined step in 0.4s which is as you say quite slow.
• I've used pointed_reduce in a few other places to simplify the proofs.
• I've added the FlFr and FFlr variants of Smash_ind which removes some boilerplate.

I'm not quite sure how to use symmetry to reduce the redundancy in the argument yet, but I will keep thinking about it.

[Alizter]

I've managed to speed up the functor_smash_homotopic proof a bit. It now takes around 0.15s.

[jdchristensen]

I just sped up a few more lines. I think this is good enough. There are still three Defined lines that are around 0.1 to 0.15s, but that's not too bad. Also, now that the proofs are shorter, I think it's ok that symmetrical arguments are repeated, since there's no simple fix for that. LGTM!