`{@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).
Require Import Category.Core Functor.Core Functor.Paths. Require Import InitialTerminalCategory.Core. Require Import NatCategory. Require Import HoTT.Basics.