Functor C (1 -> C). Proof. refine (Build_Functor C (1 -> C) (@Functors.from_terminal _ _ _ _ _) inverse_morphism_of _ _ ); abstract (path_natural_transformation; trivial). Defined.
Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Identity NaturalTransformation.Core NaturalTransformation.Paths. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors InitialTerminalCategory.NaturalTransformations. Require Import HoTT.Basics HoTT.Types.