Y : mor_of Y Y 1 = 1. Proof. simpl. erewrite IsInitialMorphism_property_morphism_unique; [ reflexivity | ]. rewrite ?, ?left_identity, ?right_identity. reflexivity. Qed.
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.