fact: Definition to_initial_category_empty `{@IsInitialCategory zero} (F : Functor C zero) : IsInitialCategory C := fun P x => initial_category_ind P (F x).
imports: Category.Core Functor.Core Functor.Paths InitialTerminalCategory.Core NatCategory HoTT.Basics