x : @functorial_morphism_of_object_of _ _ _ S T 1 1 1 1 1 x = x. Proof. let A := match goal with |- ?A = ?B => constr:(A) end in let B := match goal with |- ?A = ?B => constr:(B) end in refine (@CommaCategory.path_object' _ _ _ _ _ A B 1%path 1%path _). exact (Category.Core.right_identity _ _ _ _ @ Category.Core.left_identity _ _ _ _)%path. Defined.
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.