s d (m : morphism C s d) : morphism (1 -> C) (Functors.from_terminal _ s) (Functors.from_terminal _ d). Proof. refine (Build_NaturalTransformation (Functors.from_terminal _ s) (Functors.from_terminal _ d) (fun _ => m) _). simpl; intros. etransitivity; [ apply right_identity | symmetry; apply left_identity ]. 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.