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