`{@IsInitialCategory zero} (F G : Functor zero C) : NaturalTransformation F G := Build_NaturalTransformation F G (fun x => initial_category_ind _ x) (fun x _ _ => initial_category_ind _ x). Global Instance trunc_from_initial `{Funext} `{@IsInitialCategory zero} (F G : Functor zero C) : Contr (NaturalTransformation F G). Proof. refine (Build_Contr _ ( F G) _). abstract ( intros; apply path_natural_transformation; intro x; exact (initial_category_ind _ x) ). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors. Require Import Contractible.