`{@IsTerminalCategory one H1 H2} (F G : Functor C one) : NaturalTransformation F G := Build_NaturalTransformation F G (fun x => center _) (fun _ _ _ => path_contr _ _). Global Instance trunc_to_terminal `{Funext} `{@IsTerminalCategory one H1 H2} (F G : Functor C one) : Contr (NaturalTransformation F G). Proof. refine (Build_Contr _ ( F G) _). abstract (path_natural_transformation; exact (contr _)). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors. Require Import Contractible.