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.
added the pointers to the combinatorial proofs of the fiberwise detection of acyclicity of Kan fibrations, currently discussed on the AlgTop list, to the nLab here.
Added Kan complex as a related concept.
A structured/constructive analogue suited to purposes like homotopy type theory with equivalent homotopy theory is the notion of effective Kan fibration from
I haven’t yet found the actual definition of “effective Kan fibration” in the article, but from the discussion around it I gather it involves equipping a Kan fibration with choices of horn fillers. That concept (Kan fibrations equipped with choices of fillers) has been discussed before, under the name algebraic Kan fibrations.
I haven’t looked at the definition either, but I imagine it goes further than just requiring choices of horn fillers. To get things to work well constructively, one typically also needs to be able to relate the fillers in some ways, for example some kind of compatibilities under composition or at least identities. For example, in my thesis, which is constructive, a notion of ’normally cloven fibration’ is important (with respect to a cylinder/co-cylinder/interval), where there is an extra compatibility condition, not just a choice of lifts.
Added:
The original definition is due to Daniel M. Kan, see Definition 3.1 in
This was extended to arbitrary simplicial objects via the Yoneda embedding in Definition 3.2 of
I think you can say something stronger: if is a Kan fibration and is surjective, then is an epimorphism.
The idea is that the equivalence relation presenting is generated by , so any two vertices in the same connected component are connected by a zigzag of edges.
If and is any vertex in the connected component of , let be a zigzag from to . Since the cofibration is a weak homotopy equivalence, it lifts against . In particular there is an with , meaning is surjective in degree , and thus in all degrees by lemma 5.2 of the current version.
Assuming I’ve not made a mistake, my instinct would be to replace proposition 5.3 with this result, or maybe even to fold it into lemma 5.2. I’m not sure if that would step on what you wanted to record, though.
Good point, that’s what the entry should really say, yes. Do you want to go ahead and make the edit?
It’s also proven as Thm. 10.10 in Goerss & Jardine’s Simplicial Homotopy Theory.
1 to 16 of 16