proposition: Lemma is_initial_object__is_initial_category `(IsInitialCategory zero) (HI : P zero) : IsInitialObject (sub_pre_cat P HF) (zero; HI).
proof: Proof. typeclasses eauto. Defined.
imports: Category.Objects InitialTerminalCategory.Core InitialTerminalCategory.Functors Functor.Core Category.Strict Functor.Paths Functor.Identity Functor.Composition.Core Functor.Composition.Laws