Cone restriction along an initial functor (source code)

= Cone restriction along an initial functor

For an <initial functor> $F:\mathcal I\to\mathcal J$, restriction gives an isomorphism between the category of cones over $D:\mathcal J\to\mathcal C$ and that over $DF$. Given a cone over $DF$, choose $(i,u:Fi\to j)$ and define its $j$-leg as $D(u)\gamma_i$; connectedness of $(F\downarrow j)$ makes the result independent of the choice.