fact: Definition IsInitialMorphism_property_morphism (M : IsInitialMorphism Ap) (Y : D) (f : morphism C X (U Y)) : morphism D (IsInitialMorphism_object M) Y := CommaCategory.h (@center _ (M (CommaCategory.Build_object !X U tt Y f))).
imports: Category.Core Functor.Core Category.Dual Functor.Dual Category.Objects InitialTerminalCategory.Core InitialTerminalCategory.Functors Trunc Types.Sigma HoTT.Tactics Basics.Tactics