Cocone extension along a final functor

ID: cocone-extension-along-a-final-functor

Let be final and . A cocone extends uniquely to : for , choose in and set . Connectedness makes this independent of the choice. Consequently
whenever either side is constructed by this universal property.

New to topics? Read the docs here!