Cone restriction along an initial functor

ID: cone-restriction-along-an-initial-functor

For an initial functor , restriction gives an isomorphism between the category of cones over and that over . Given a cone over , choose and define its -leg as ; connectedness of makes the result independent of the choice.

New to topics? Read the docs here!