functor__of__initial_morphism -| G. Proof. refine (adjunction_unit_counit__of__adjunction_unit _). eexists (Build_NaturalTransformation 1 (G o functor__of__initial_morphism) (fun x => IsInitialMorphism_morphism (@HM x)) (fun s d m => symmetry _ _ (IsInitialMorphism_property_morphism_property (@HM s) _ _))). simpl. exact (fun c => @IsInitialMorphism_property _ _ c G (M c) (@HM c)). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Identity Functor.Composition.Core. Require Import Functor.Dual Category.Dual. Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.UnitCounitCoercions Adjoint.Dual. Import Comma.Core. Require Import UniversalProperties Comma.Dual InitialTerminalCategory.Core InitialTerminalCategory.Functors.