(lim_obj : C) (lim_mor : morphism (D -> C) (diagonal_functor' C D lim_obj) F) (lim := CommaCategory.Build_object (diagonal_functor C D) !(F : object (_ -> _)) !lim_obj (center _) lim_mor) (UniversalProperty : forall (lim_obj' : C) (lim_mor' : morphism (D -> C) (diagonal_functor' C D lim_obj') F), Contr { m : morphism C lim_obj' lim_obj | lim_mor o morphism_of (diagonal_functor' C D) m = lim_mor' }) : IsTerminalMorphism lim. Proof. apply Build_IsTerminalMorphism. intros A' p'. specialize (UniversalProperty (A' (center _))).*) End Limit.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core. Require Import ExponentialLaws.Law1.Functors FunctorCategory.Core. Require Import KanExtensions.Core InitialTerminalCategory.Core NatCategory. Require Import Functor.Paths. Import Comma.Core.