fact: Definition modification_help_alt (F₁ F₂ : functor_data B₁ B₂) (α : nat_trans_data F₁ F₂) (X : B₁) : (rassociator (id₁ (F₁ X)) (id₁ (F₁ X)) (α X)) • (id₁ (F₁ X) ◃ (lunitor (α X) • rinvunitor (α X))) • lassociator (id₁ (F₁ X)) (α X) (id₁ (F₂ X)) • ((lunitor (α X) • rinvunitor (α X)) ▹ id₁ (F₂ X)) • rassociator (α X) (id₁ (F₂ X)) (id₁ (F₂ X)) • (α X ◃ lunitor (id₁ (F₂ X))) = (lunitor (id₁ (F₁ X)) ▹ α X) • lunitor (α X) • rinvunitor (α X).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Univalence UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.Display.Base UniMath.Bicategories.PseudoFunctors.Display.Map1Cells UniMath.Bicategories.PseudoFunctors.Display.Map2Cells UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.StrictPseudoFunctor UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.Modifications.Modification UniMath.Bicategories.PseudoFunctors.Examples.StrictToPseudo UniMath.Bicategories.PseudoFunctors.Examples.Identity UniMath.Bicategories.PseudoFunctors.Examples.Composition