x : (functorial_morphism_of TA' TB' o functorial_morphism_of TA TB)%functor x = functorial_morphism_of TA'' TB'' 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 _). subst AF'' BF'' CF'' TA'' TB''. simpl in *. abstract ( autorewrite with morphism; simpl; helper (exact idpath) (commutes TA') (commutes TB') ). 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.