fact: Definition to_terminal `{@IsTerminalCategory one Hone Hone'} : Functor C one := Build_Functor C one (fun _ => center _) (fun _ _ _ => center _) (fun _ _ _ _ _ => contr _) (fun _ => contr _).
imports: Category.Core Functor.Core Functor.Paths InitialTerminalCategory.Core NatCategory HoTT.Basics