proposition: Lemma p_composition_of_coherent_iso_for_rewrite w x y z (f : morphism C w x) (g : morphism C x y) (h : morphism C y z) : (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ F w z) (Category.Core.associativity C w x y z f g h))) = @Build_Isomorphic (_ -> _) _ _ ((((p_composition_of F w y z h (g o f))^-1) o ((p_morphism_of F h oL (p_composition_of F w x y g f)^-1) o ((associator_1 (p_morphism_of F h) (p_morphism_of F g) (p_morphism_of F f)) o ((p_composition_of F x y z h g oR p_morphism_of F f) o p_composition_of F w x z (h o g) f)))))%natural_transformation p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper.
proof: Proof. apply path_isomorphic; simpl. simpl rewrite (@p_composition_of_coherent _ C F w x y z f g h). exact p_composition_of_coherent_for_rewrite_helper. 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