w x y z (f : morphism C w x) (g : morphism C x y) (h : morphism C y z) (p p0 p1 p2 : PreCategory) (f0 : morphism C w z -> Functor p2 p1) (f1 : Functor p0 p1) (f2 : Functor p2 p) (f3 : Functor p p0) (f4 : Functor p2 p0) `(@IsIsomorphism (_ -> _) f4 (f3 o f2)%functor n) `(@IsIsomorphism (_ -> _) (f0 (h o (g o f))%morphism) (f1 o f4)%functor n0) : @paths (NaturalTransformation _ _) (@morphism_isomorphic _ _ _ (Category.Morphisms.idtoiso (p2 -> p1) (ap f0 (Category.Core.associativity C w x y z f g h)))) (n0^-1 o ((f1 oL n^-1) o ((f1 oL n) o (n0 o (@morphism_isomorphic _ _ _ (Category.Morphisms.idtoiso (p2 -> p1) (ap f0 (Category.Core.associativity C w x y z f g h))))))))%natural_transformation. Proof. simpl in *. let C := match goal with |- @paths (@NaturalTransformation ?C ?D ?F ?G) _ _ => constr:((C -> D)%category) end in apply (@iso_moveL_Vp C); apply (@iso_moveL_Mp C _ _ _ _ _ _ (iso_whisker_l _ _ _ _ _ _ _)). path_natural_transformation. reflexivity. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Morphisms FunctorCategory.Morphisms. Require Import Functor.Composition.Core. Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import NaturalTransformation.Isomorphisms. Require Import NaturalTransformation.Paths. Require Import FunctorCategory.Core. Require Import Pseudofunctor.Core. Require Import HoTT.Tactics.