proposition: Lemma p_composition_of_coherent_for_rewrite_helper 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: 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.
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Morphisms FunctorCategory.Morphisms Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Isomorphisms NaturalTransformation.Paths FunctorCategory.Core Pseudofunctor.Core HoTT.Tactics