Timeline for Why is the path fibration a strong Hurewicz fibration?
Current License: CC BY-SA 3.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 8, 2015 at 10:07 | vote | accept | Andrej Bauer | ||
| Jul 8, 2013 at 17:03 | comment | added | Peter May | I assume that I have a forgetful functor, U say, from M to V. A map f in M is an r-equivalence if Uf is an h-equivalence. It is a q-equivalence if Uf is a q-equivalence. In our algebraic context, V has h and r model structures that happen to coincide, which makes the definition look more natural. | |
| Jul 8, 2013 at 5:21 | comment | added | Karol Szumiło | Just to make sure: by underlying (weak) homotopy equivalences in a $\mathcal{V}$-enriched categories do you mean morphisms inducing (weak) homotopy equivalences on all (fibrant?) representables? Or does it depend on the notion of a "structured" object? | |
| Jul 8, 2013 at 1:35 | history | edited | Peter May | CC BY-SA 3.0 |
added 841 characters in body
|
| Jul 7, 2013 at 8:35 | comment | added | Karol Szumiło | I, for one, would like to read more about these six model structures. | |
| Jul 7, 2013 at 6:29 | comment | added | Andrej Bauer | Thanks for the comments. I was aware of the problems you mention in the last paragraph, as my starting point was Barthel & Rhiel. I might as well explain what I am doing. I am trying to get Hurewicz style model structure inside extensional type theory, or in categorical terms in a locally cartesian closed category. This in particular means no excluded middle in general. The consequence is bizarre: paths cannot be concatenated as usual. But I have a cunning plan (which involves the lccc structure in an essential way), which however involves checking a lot of details. | |
| Jul 6, 2013 at 23:28 | history | edited | Peter May | CC BY-SA 3.0 |
deleted 1 characters in body
|
| Jul 6, 2013 at 21:48 | history | answered | Peter May | CC BY-SA 3.0 |