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). Proof. rewrite !vassocl. rewrite lunitor_lwhisker. rewrite rwhisker_vcomp. rewrite !vassocl. rewrite rinvunitor_runitor, id2_right. refine (!_). etrans. { rewrite rinvunitor_natural, <- rwhisker_hcomp. apply idpath. } rewrite !vassocr. apply maponpaths_2. rewrite !vassocl. rewrite <- lwhisker_vcomp. rewrite !vassocl. rewrite rinvunitor_triangle. rewrite !vassocr. apply maponpaths_2. rewrite lunitor_lwhisker. rewrite runitor_lunitor_identity. apply idpath. Qed. Local Definition psfunctor_to_functor_data (F : psfunctor B₁ B₂) : functor_data B₁ B₂. Proof. use make_functor_data. - exact (λ X, F X). - exact (λ _ _ f, #F f). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.StrictPseudoFunctor. Import PseudoFunctor.Notations. Import StrictPseudoFunctor.Notations. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.PseudoFunctors.Examples.StrictToPseudo. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.