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.
1 to 6 of 6