flattening for pushouts + total space of Hopf construction

[Alizter]

We use the colimits library to prove flattening for pushouts. The proof is a bit annoying as it doesn't compute well.

We use this to show that the Hopf construction has total space equivalent to a join. Because of the uncomputable nature of the flattening lemma we are unable to show that it preserves the base point.

This should be enough for something else I am working on. Corollaries like the Hopf fibrations for the spheres would ideally come once we sort out the computability.

I tried proving the flattening lemma directly for GraphQuotient and Pushout but I was not able to get around the difficult path algebra easily. The fact that this is done in the Colimits library is good and we should use it, however it is not as easy as I thought to transfer across equivalences in this case. Maybe I am missing something obvious?

[jdchristensen]

I'll take a closer look later.

[jdchristensen]

There's some relevant discussion about different flattening lemmas here: #1833

It would be nice if some redundancies could be removed, but that can be future work.

[jdchristensen]

I think the top of PushoutFlattening.v and Colimit_Pushout_Flattening.v should have comments referring to the other file, and explaining what is different between them: the first is for a pushout defined directly as a coequalizer, and the second is for a pushout defined as a special case of Colimit (which is itself defined as a coequalizer).

BTW, do the problems with computability go right back to Colimit_Flattening.v, or do they arise from something in this PR?

[Alizter]

BTW, do the problems with computability go right back to Colimit_Flattening.v, or do they arise from something in this PR?

@jdchristensen I think it stems from this PR, though I haven't really computed with the other flattening lemma yet. Upon inspection, I don't see any reason why it should struggle, although there are a lot more terms to unfold compared to proving it directly.

There's some relevant discussion about different flattening lemmas here: #1833

It would be nice if some redundancies could be removed, but that can be future work.

I initially experimented with deriving the flattening lemma for coequalizers using the statement of one for GraphQuotient but it wasn't entirely obvious how to proceed. The main issue is adapting the family being flattened as even very similar types have long arguments to show that their families using univalence agree.

[Alizter]

OK the main performance problems come from Colimit_Pushout_Flattening.PO_flattening I've managed to make a shorter proof of PushoutFlattening.pushout_coh that seems to compute ok. There is basically a very large path induction in PO_flattening which is never going to compute in any reasonable case due to the sheer size of the terms involved. I'll see if I can tweak this to be more direct.

[jdchristensen]

If you add these two results to the end of Colimit_Pushout.v (still inside the Section):

  Definition equiv_pushout_PO_beta_pglue (a : A)
    : ap equiv_pushout_PO (pglue a) = popp a.
  Proof.
    cbn.
    refine (_ @ _).
    1: nrapply Pushout_rec_beta_pglue.
    unfold popp'; cbn.
    rewrite 2 concat_1p.
    reflexivity.
  Defined.

  Definition Pushout_rec_PO_rec (P : Type) (pushb : B -> P) (pushc : C -> P)
    (pusha : forall a : A, pushb (f a) = pushc (g a))
    : Pushout_rec P pushb pushc pusha == PO_rec P pushb pushc pusha o equiv_pushout_PO.
  Proof.
    snrapply Pushout_ind.
    1, 2: reflexivity.
    intro a; cbn beta.
    nrapply transport_paths_FlFr'; apply equiv_p1_1q.
    lhs exact (Pushout_rec_beta_pglue P pushb pushc pusha a).
    symmetry.
    lhs nrapply (ap_compose equiv_pushout_PO _ (pglue a)).
    lhs nrapply (ap _ (equiv_pushout_PO_beta_pglue a)).
    nrapply PO_rec_beta_pp.
  Defined.

then the proof of flattening_coh is easy:

  Lemma flattening_coh
    : forall x, pushout_flattening_fam x <~> POCase_P A0 B0 C0 f0 g0 (equiv_pushout_PO x).
  Proof.
    intro x.
    apply equiv_path.
    nrapply Pushout_rec_PO_rec.
  Defined.

[jdchristensen]

The two new results don't require Univalence. They require Funext, but only because equiv_pushout_PO does. And we're only using the map underlying this equivalence, which doesn't need Funext. So it would be possible to work with this underlying map instead and avoid Funext if you want.

[Alizter]

@jdchristensen I've just pushed my changes from earlier today. I haven't had time to address your later comments just yet. Some of these commits could be dropped as I was experimenting with alternative proofs. We can clean them up when we decide which is best.

[Alizter]

@jdchristensen Thanks for your suggestion, it seems to work well! I've removed the old coherence results accordingly now as the new proof is much nicer.

[Alizter]

I've added some comments about the differences between the two flattening lemmas and addressed some of Dan's recent comments.

[jdchristensen]

About computing with PO_flattening, I think we'd like a lemma of the form

  Definition PO_flattening_beta_pol
    : PO_flattening o pol == functor_sigma pol (fun _ => idmap).

This typechecks, and I was hoping it was definitionally true. I tried with one of the proofs of PO_flattening, and it wasn't definitional, but maybe with a different proof it will be. Certainly there's no fundamental reason why the underlying map of PO_flattening isn't the obvious thing, so I'm a bit puzzled here.

[jdchristensen]

About computing with PO_flattening, I think we'd like a lemma of the form

  Definition PO_flattening_beta_pol
    : PO_flattening o pol == functor_sigma pol (fun _ => idmap).

Looking at the proof of flattening_lemma (for general colimits), it looks to me like the underlying map will compute definitionally on point constructors to the expected thing (basically as described in cocone_E'). So that's the first place we should try to write down the beta rule. If it works, then we should be able to use that to prove a beta rule for PO_flattening. For simplicity, we might restrict to point constructors.

[Alizter]

@jdchristensen It seems that there are various heavy terms in PO_flattening that cause Coq to struggle when unfolding. I agree that having a computation lemma would be good. I believe the obstruction to that falling out definitionally however stems from Colimit_Flattening.v.

By the way, I've added the Hopf entries to HoTTBook.v.

[Alizter]

Another useful consequence of this equivalence computing is that we can describe the Hopf map directly from the join to the suspension (without univalence or H-space multiplication being an equivalence) and show it is homotopic to the projection composed with the equivalence (also pointed). This would also let us show the fiber of that map is X.

[jdchristensen]

This looks great! I think it's good to merge this now, and to think about the computation issues in a future PR.