p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper' : @IsIsomorphism (_ -> _) _ _ (n2 ^-1 o (f2 oL n1 ^-1 o (associator_1 f2 f1 f3 o (n0 oR f3 o n))))%natural_transformation. Proof. eapply isisomorphism_compose; [ eapply isisomorphism_inverse | eapply isisomorphism_compose; [ eapply iso_whisker_l; eapply isisomorphism_inverse | eapply isisomorphism_compose; [ typeclasses eauto | eapply isisomorphism_compose; [ eapply iso_whisker_r; typeclasses eauto | typeclasses eauto ] ] ] ]. Defined.
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.