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. 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.
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.