`{Funext} : @functorial_morphism_of _ _ _ S T 1 1 1 1 1 = 1%functor. Proof. path_functor; simpl. exists (path_forall _ _ functorial_identity_of_helper). simpl. functorial_helper_t functorial_identity_of_helper. Qed.
Require Import Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core. Require Import NaturalTransformation.Composition.Laws. Require Import Functor.Paths. Require Import Category.Strict. Import Comma.Core. Import Functor.Identity.FunctorIdentityNotations NaturalTransformation.Identity.NaturalTransformationIdentityNotations. Require Import HoTT.Tactics PathGroupoids Types.Forall.