Proving Lemma 8.5.5

[Alizter]

I have been stuck on this for a few weeks now:

Section HSpace.
(*   Context `{Funext}. *)

  Class IsHSpace (space : Type) := {
    id : space;
    mu : space -> space -> space;
    left_id : forall a, mu id a = a;
    right_id : forall a, mu a id = a
  }.

  Context {A : Type}
         `{IsHSpace A}
         `{IsConnected 0 A}.

  Lemma mu_l_equiv' : forall (a : A), IsEquiv (mu a).
  Proof.
    intro.
  Admitted.

  Lemma mu_r_equiv' : forall (a : A), IsEquiv (fun x => mu x a).
  Proof.
    serapply (conn_map_elim -1).
  Admitted.

It is quite difficult to follow the book proof, as it is not so specific. Any pointers on how to prove this?

[Alizter]

So I have this lemma

 Lemma conn_map_from_unit (n : trunc_index) (A : Type) (a : A)
          `{IsConnected n.+1 A}
  : IsConnMap n (@const Unit A a).
  Proof.
    intro b.
    apply (isconnected_equiv' n _ (hfiber_const_equiv a b)^-1). 
    apply (contr_equiv' ((Trunc n) (a = b))).
    reflexivity.
    exact (contr_trunc_conn n).
  Defined.

which I could probably put in reflective subuniverse but I might need some help with that. Anyway it allows me to get this far:

Lemma mu_l_equiv' : forall (a : A), IsEquiv (mu a).
  Proof.
    pose (P := fun a => BuildhProp (IsEquiv (mu a))).
    serapply (@conn_map_elim -1 Unit A _ (@conn_map_from_unit -1 _ id H0) P).
    +

And the goal is:

1 subgoal
A : Type
H : IsHSpace A
H0 : IsConnected 0 A
P := fun a : A => BuildhProp (IsEquiv (H.(mu) a)) : A -> hProp
______________________________________(1/1)
forall a : Unit, (fun a0 : A => (P a0).(trunctype_type)) (const H.(id) a)

What I should do now is turn P into an equivalent family P' as hProp is set-truncated, so I can just set-truncate a. Then as it is 0-connected it will be contractable so I only need prove for a base point. Which we have in the definition of HSpace anyway.

---

Here are my problems:

I can't find anything about the universal property of truncation in the library.

The proof gets very technical and even in the Agda and Lean implementations it is slightly clearer. We might be able to shorten this proof but it seems to me this kind of proof technique isn't very well supported.

In Brunerie's thesis for example there is a short and sweet proof of this face:

"What we want to prove is a mere proposition depending on a : A. Given that A is pointed and 0-connected, it is enough to prove it for the base point a. But the functions mu(a, -) and mu(-,a) are both equal to the identity function, hence they are equivalences."

What can we do so that we don't have to jump through this many hoops to say the above in coq?

[mikeshulman]

i'll look at the rest of it when I have a chance, but your lemma is conn_point_incl in HIT/Connectedness.v.

[mikeshulman]

Ok, here's how I would do it:

  Lemma mu_l_equiv' `{Univalence} : forall (a : A), IsEquiv (mu a).
  Proof.
    refine (conn_map_elim -1 (unit_name id) _ _).
    refine (conn_point_incl id).
    exact _.                    (* Why didn't Coq find this? *)
    intros _.
    refine (isequiv_homotopic idmap _).
    intro a; symmetry; apply left_id.
  Defined.

I think that's a pretty clear translation of Brunerie's proof. (Not sure why Coq didn't find the instance of HSpace, though.)

[Alizter]

That's working nicely thanks!

That is a bit strange why Coq couldn't find it though.

I have my Hopf fibration formalisation here.

I am stuck on this supposedly simple lemma of showing susp is a special kind of pushout.

 (** The suspension ΣX can be written as a pushout: 1 ⊔_X 1 **)
  Lemma susp_equiv_pushout : Susp X <~> pushout (@const X _ tt) (const tt).

at ln 180.

After that I have

• The total space of the pushout fibration is the pushout of the total spaces of the components (ln 84)
• Compute the fiber and total space of the hopf construction as A and A*A (ln 218).

Once all these are done we should have the Hopf fibration formalised in coq.

[mikeshulman]

Well, it looks like your next step in susp_equiv_pushout should be rewrite ap_compose. It seems like Coq has some trouble figuring out how to apply the beta rules after that though, I guess some of the implicit arguments may have to be given explicitly.

I wonder, though, whether it wouldn't be a better idea in the long run to redefine Susp to be that pushout by definition.

[Alizter]

@mikeshulman I would be in favor of defining suspension as such, just as long as we keep it under the covers. Similar to how circle is defined as an equalizer.

I've started a branch off master to see what will happen.

[Alizter]

So this seems to be ok for the most part. I've gone ahead an redefined suspension without breaking its uses. It only fails to compile because issect_Sph2_to_S2 does something weird. I can't tell what it is though.

[mikeshulman]

Well, I have no idea why it broke, but changing the problematic line to

  refine ((transport_paths_FlFr (f := fun y => y) _ _) @ _).

seems to work.

[Alizter]

Nice, I will go ahead and make a pull request for these changes.

[mikeshulman]

Although now there is a test that fails: apparently we never got around to ensuring that our definition of coequalizer lives in the correct universe. The definition should be something like

  Private Inductive Coeq {B A : Type@{i}} (f g : B -> A) : Type@{i} :=
  | coeq : A -> Coeq f g.

[Alizter]

Yes I just noticed that too. I will change this.

[Alizter]

OK on my nhomotopy branch I have merged the change to suspension so I can play with it. I am however completely stuck at proving the flattening type is equal to a pushout.

And computing the fiber and total space of the hopf fibration isn't going so well. Something interesting to note, when using "compute" in the total space lemma coq gets stuck and stats evaluating something forever as far as I can tell. This has happened on 3 machines that I've tested.

I am wondering if the type Wtil can be written in terms of coequalizers (I am not sure). That would make computation easier here.

[mikeshulman]

It'll be a while before I have a chance to look at this, sorry -- semester starting.

But the idea of the flattening lemma is indeed that the total space of a fibration over a coequalizer should itself be a coequalizer.

[Alizter]

@mikeshulman How can I write Wtil as a coequalizer? What are some helpful references for building HITs out of pushouts and coequalizers? Doesn't have to be about coq, I am struggling to do this on paper.

[mikeshulman]

Look at the definition of Wtil in section 6.12 of the book, and use the left universal property (2.15.9) of Sigma-types to rewrite its constructors in the form of a coequalizer.

What sort of HITs do you want to build out of pushouts and coequalizers?

[Alizter]

2.15.9 has sorted it out! This is essentially "dependent uncurrying" right?

How can you be certain when something can be built out of pushouts and coequalizers is really what I was getting at. I know you have a counter example in your semantics of HITs paper, which I never really read it in detail since it was a bit daunting. As I understand your counter example works by constructing an inaccessable cardinal. Most HITs that I will write down when doing homotopy theory probably won't do this, so does that necessarily mean they can be written as coequalizers? Will I be able to do this by fiddling around with constructors till they match a HIT I know?

But for the context of Wtil, I don't think it was a question of "can it be written as a coequalizer" but "how". Thanks for pointing me to 2.15.9 this means I can continue for a bit. :-)

[mikeshulman]

Yes, "dependent uncurrying" is a good thing to call it.

In general, any nonrecursive HIT can be built out of pushouts (or equivalently coequalizers, since -- at least in the presence of coproducts -- pushouts and coequalizers can be built out of each other). Nonrecursive means that none of the constructors take inputs from the HIT being defined. Some apparently-recursive HITs can also be built out of pushouts in less obvious ways, such as truncations and localizations at maps between omega-compact types, but those require more cleverness.

[Alizter]

So I've had a go at rewriting Wtil as a coequalizer. I am stuck on proving Wtil_ind_betappt however. There is some rewriting that needs to be done but I am not seeing it. I want to rewrite using ppt' as I can see the subexpression is in that form however ppt' is written with (;_) but my expression has pr's. I do not know how to proceed here.

[mikeshulman]

I would start with rewrite (Coeq_ind_beta_cp Q _ _ (b;y)); cbn.

[Alizter]

@mikeshulman Thanks, I have managed to finish it now. Funnily enough, looking back through the pushout of total spaces is total space of pushout fibrations lemma it seems I didn't need Wtil to be a coequalizer after all. However in the future, if we ever need to do a double flattening for whatever reason it may be useful. So I have kept it in my branch flatten, but I don't think its worth pulling here yet since there is no added benefit. There are lots of comments in Flattening.v saying how it should be moved to the coeq file and later derived for pushouts etc. This may be more desirable anyhow.

Now I am stuck trying to compute the fiber and total space of the "fibration over the suspension". I need to think about it some more. :-)

[Alizter]

Something to make note of in case I forget:

The Hopf construction doesn't need to be done on a 0-connected type but rather any type that makes its H-space multiplication into equivalences. In particular every 0-connected type does this, but so does S0 which is not 0-connected. This means that the Hopf construction works for S0 and there is no special case anymore.