characterize fiber of loop-susp counit

[Alizter]

We characterize the fiber of the loop-susp counit. We can't make it a pointed equivalence just yet as we are missing pointedness of the Hopf construction. Interestingly we have to twist the first component when we try to show the sigma types are equivalent.

I've also gone ahead and added the lemmas in #1841 as we use one of these.

[Alizter]

I've been a bit lazy by using rewrite in the proof however I am not too concerned about it for the time being as it won't compute due to the Hopf equivalence anyway. I'll add a note to use explicit path algebra when that business is sorted out.

[jdchristensen]

This is great to have! Are you planning on adding a corollary that says that if X is n-connected, then the loop-susp conunit is roughly 2n-connected?

[Alizter]

@jdchristensen I can add that corollary too.

[Alizter]

@jdchristensen I wrote down the corollary but I only managed to do it for n.+2 connected types. Do you think it can be strengthened to n.+1? In order to use the equivalence I have to use the lemmas about connectedness and checking only the base point.

[Alizter]

FTR do we know what the fibers and cofibers of the unit and counit are? I'm having trouble finding these results in AT textbooks. Freudenthal obviously says that we have an 2n-connected fiber for the unit, but I'm not sure if this is a smash or a join, I'm a little confused about the connectedness indexing. I don't recall ever coming across those characterisations. I have even less idea about the cofibers.

[jdchristensen]

I wrote down the corollary but I only managed to do it for n.+2 connected types. Do you think it can be strengthened to n.+1?

If X is (-1)-connected, the corollary would say that the fibre is (-2)-connected. Since every type is (-2)-connected, this is trivially true. So you can extend it one step down, but you might have to break the proof into two cases.

I don't know the answers to the other questions off the top of my head.

[jdchristensen]

BTW, while you are adding those results about transport, here's another one I had lying around:

(** This is an improvement to [transport_arrow_toconst].  That result shows that the functions are homotopic, but even without funext, we can prove that these functions are equal. *)
Definition transport_arrow_toconst' {A : Type} {B : A -> Type} {C : Type}
  {x1 x2 : A} (p : x1 = x2) (f : B x1 -> C)
  : transport (fun x => B x -> C) p f = f o transport B p^.
Proof.
  destruct p; auto.
Defined.

I assume that a similar thing can be done for fromconst.

[Alizter]

@jdchristensen Thanks that works. I've also added the other transport lemma.

[jdchristensen]

This looks good to me. I restarted one job that failed with a download glitch, and it worked.