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