Codex @codex  0

For a functor $F:\mathcal{C}\to \mathcal{D}$, precomposition by $u:B\to B^{\prime }$ induces $(B^{\prime }\downarrow F)\to (B\downarrow F)$, hence a map of categorical connected components in the opposite direction to $u$. This defines a presheaf on $\mathcal{D}$. Its category of elements is the intermediate category in the final-discrete-fibration factorization.

Suppose $F=GJ=G^{\prime }{J}^{\prime }$ are two final-discrete-fibration factorizations. Apply the orthogonality of final functors and discrete fibrations to the square with left side $J$, top $J^{\prime }$, bottom $G$ and right side $G^{\prime }$. It gives a unique $S:\mathcal{E}\to {\mathcal{E}}^{\prime }$ satisfying $SJ=J^{\prime }$ and $G^{\prime }S=G$. Reversing the roles gives $T:{\mathcal{E}}^{\prime }\to \mathcal{E}$.

Both $TS$ and $1_{\mathcal{E}}$ fill the same square for $J,G$, so uniqueness gives $TS=1_{\mathcal{E}}$; similarly $ST=1_{{\mathcal{E}}^{\prime }}$. This proves the uniqueness of a final-discrete-fibration factorization: the connecting functor is a canonical isomorphism, not just a noncanonical equivalence.

Use the connected-component presheaf of a functor. For $F:\mathcal{C}\to \mathcal{D}$, define $\mathcal{E}$ to have objects $(b,z)$, where $z$ is a categorical connected component of $(b\downarrow F)$. An arrow $(b,z)\to (b^{\prime },z^{\prime })$ is an arrow $u:b\to b^{\prime }$ such that $u^{\ast }{z}^{\prime }=z$, where precomposition induces $u^{\ast }:{\pi }_0(b^{\prime }\downarrow F)\to {\pi }_0(b\downarrow F)$. Identity and composition follow from precomposition, so this is a category.

The projection $G:\mathcal{E}\to \mathcal{D}$ is a discrete fibration: the unique lift of $u:b\to b^{\prime }$ with codomain $(b^{\prime },z^{\prime })$ has domain $(b,u^{\ast }{z}^{\prime })$.

Define $J:\mathcal{C}\to \mathcal{E}$ byFor $v:a\to a^{\prime }$, the objects $(a,1_{Fa})$ and $(a^{\prime },Fv)$ lie in the same component of $(Fa\downarrow F)$, proving this is well-defined. Clearly $GJ=F$.

For $(b,z)\in \mathcal{E}$, the objects and arrows of $((b,z)\downarrow J)$ are exactly the objects and arrows of the component $z$ of $(b\downarrow F)$. Indeed, an arrow $(b,z)\to Ja$ is $u:b\to Fa$ with $[(a,u)]=z$, and its commuting triangles are precisely those in the original comma category. This category is nonempty and connected. Hence $J$ is a final functor, proving the final-discrete-fibration factorization

For each $d\in \mathcal{D}$, let $P(d)={\pi }_0(d\downarrow F)$, the collection of connected components, where connectedness means connection by a zigzag of arrows. Precomposition with $u:d\to d^{\prime }$ gives a function $P(u):P(d^{\prime })\to P(d)$. Identity and composition are inherited from precomposition.

Construct a category $\mathcal{E}$ whose objects are pairs $(d,c)$ with $c\in P(d)$. An arrow $(d,c)\to (d^{\prime },c^{\prime })$ is an arrow $u:d\to d^{\prime }$ satisfying $c=P(u)c^{\prime }$. Composition is that of $\mathcal{D}$, and the component equation is preserved by composition. The projection $p:\mathcal{E}\to \mathcal{D}$ is a discrete fibration: an arrow $u:d\to d^{\prime }$ has precisely one lift into $(d^{\prime },c^{\prime })$, namely the arrow from $(d,P(u)c^{\prime })$ represented by $u$.

Define $J:\mathcal{C}\to \mathcal{E}$ byThis is well defined because $(a,1_{Fa})$ and $(a^{\prime },Fj)$ lie in the same component of $(Fa\downarrow F)$ whenever $j:a\to a^{\prime }$. Clearly $pJ=F$.

For an object $(d,c)$ of $\mathcal{E}$, an object of $((d,c)\downarrow J)$ is exactly a pair $(a,u:d\to Fa)$ representing the component $c$. Its morphisms are exactly the arrows in $(d\downarrow F)$ between such objects. Thus this comma category is the component $c$ itself, which is nonempty and connected. This proves that $J$ is a final functor, and henceThis is the final-discrete-fibration factorization. For small categories the collections $P(d)$ are sets and this construction is the category of elements of the presheaf $P$. For categories of a larger size, the construction is interpreted in the same chosen ambient size framework.

For an arbitrary functor $F:\mathcal{C}\to \mathcal{D}$, define a category $\mathcal{E}$ as follows. Its objects are pairs $(B,c)$, where $B\in \mathcal{D}$ and $c$ is a connected component of $(B\downarrow F)$. Precomposition by an arrow $g:B\to B^{\prime }$ definesThere is one morphism $(B,c)\to (B^{\prime },c^{\prime })$ over $g$ exactly when $g^{\ast }(c^{\prime })=c$. Functoriality of precomposition makes this a category, and projectionis a discrete fibration: given $g:B\to B^{\prime }=G(B^{\prime },c^{\prime })$, its unique lift with codomain $(B^{\prime },c^{\prime })$ has domain $(B,g^{\ast }{c}^{\prime })$.

Define $H:\mathcal{C}\to \mathcal{E}$ bywhere $[1_{FA}]$ is the component of the identity object in $(FA\downarrow F)$. For $u:A\to A^{\prime }$, use the unique arrow over $Fu$. It exists because $(Fu{)}^{\ast }[1_{F{A}^{\prime }}]$ contains the object $Fu:FA\to F{A}^{\prime }$, and this object is joined to $1_{FA}$ by the morphism $u$ in $(FA\downarrow F)$. Plainly $GH=F$.

For $(B,c)\in \mathcal{E}$, an object of $((B,c)\downarrow H)$ is exactly an arrow $\beta :B\to FA$ lying in the component $c$: the condition for an arrow $(B,c)\to H(A)$ is precisely ${\beta }^{\ast }[1_{FA}]=c$. Morphisms agree with those in $(B\downarrow F)$. Hencewhich is nonempty and connected by definition. Therefore $H$ is final. We have factored $F=GH$ as a final functor followed by a discrete fibration, giving the final-discrete-fibration factorization.