The quasi-fibration section had an off-by-one error in the range of indices.

]]>The current version of Riehl-Verity, v4, does not contain the proof, but it cites v2 of itself for the proof.

]]>It’s also proven as Thm. 10.10 in Goerss & Jardine’s *Simplicial Homotopy Theory*.

Dan Quillen, The geometric realization of a Kan fibration is a Serre fibration, Proc. AMS 19 (1968), 1499–1500

which is remarkably terse. Is there a more revelatory proom somwhere? ]]>

cross-linked (here) the discussion of surjective Kan fibrations with the respective discussion of acyclic Kan fibrations

]]>I have made the edit now.

]]>Good point, that’s what the entry should really say, yes. Do you want to go ahead and make the edit?

]]>I think you can say something stronger: if $f : X \to Y$ is a Kan fibration and $\pi_0(X) \to \pi_0(Y)$ is surjective, then $f$ is an epimorphism.

The idea is that the equivalence relation presenting $Y_0 \to \pi_0(Y)$ is generated by $Y_1$, so any two vertices in the same connected component are connected by a zigzag of edges.

If $x \in X_0$ and $y \in Y_0$ is any vertex in the connected component of $f(x)$, let $Z \to Y$ be a zigzag from $f(x)$ to $y$. Since the cofibration $\Delta^0 \to Z$ is a weak homotopy equivalence, it lifts against $f$. In particular there is an $x'$ with $f(x') = y$, meaning $f$ is surjective in degree $0$, 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.

]]>I have added some basic remarks on surjective Kan fibrations (now here) to record the fact that every $\pi_0$-epi into a Kan complex may be resolved by a surjective Kan fibration.

]]>Added:

The original definition is due to Daniel M. Kan, see Definition 3.1 in

- Daniel M. Kan,
*A combinatorial definition of homotopy groups*, The Annals of Mathematics 67:2 (1958), 282–312. doi.

This was extended to arbitrary simplicial objects via the Yoneda embedding in Definition 3.2 of

- Daniel M. Kan,
*On c.s.s. categories*, Boletín de la Sociedad Matemática Mexicana 2 (1957), 82–94. PDF.

added the example of the empty bundle (here)

]]>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.

]]>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*.

A structured/constructive analogue suited to purposes like homotopy type theory with equivalent homotopy theory is the notion of effective Kan fibration from

- Benno van den Berg, Eric Faber,
*Effective Kan fibrations in simplicial sets*, arXiv:2009.12670 - Benno van den Berg,
*Effective Kan fibrations in simplicial sets*, Bohemian Logical & Philosophical Café, Feb 2021, yt

Added Kan complex as a related concept.

]]>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.

]]>