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