Finality of a functor (source code)

= Finality of a functor
{title2=$\pi_0(b\downarrow F)=1\text{ for every }b$}

= Finality
{synonym}

The finality property of a <functor> means every required <comma category> is nonempty and connected. It is the condition defining a <final functor>; the displayed criterion uses <categorical connected components>.