Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 6 of 6
In the context of the discussion at infinity-action, given some and some , consider as equipped with the canonical -action. Given any we have a homotopy pullback of the form
I am sure that the left vertical map here is the one known as . But I am being dense and lacking a real formal proof. What’s a good formal proof of this?
Well, the pullback square exhibiting as the fiber of induces this map by the universal property…
How do you see this?
I am talking about identifying the universal map as the one given by restricting to equivalences the map formed by actual composition.
Is this obvious? What am I missing?
I think it should follow by unraveling the universal property and using the fact that the equivalence corresponding to a point of is also the path living in the homotopy pullback square exhibiting as . I don’t have time to write it out carefully right now.
So that’s why I said I am sure that it works, but that I don’t have a fully formal proof.
Sorry, I didn’t mean to ask you to do this work for me. Though I thought I’d try and see if you see this within microseconds. :-)
Sorry. (-:
1 to 6 of 6