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. Consequentlywhenever either side is constructed by this universal property.
New to topics? Read the docs here!