Definition make_is_invertible_modification {B B' : bicat} {F G : psfunctor B B'} {σ τ : pstrans F G} (m : modification σ τ) (Hm : ∏ (X : B), is_invertible_2cell (m X)) : is_invertible_modification m. Proof. use make_is_invertible_2cell. - use make_modification. + exact (λ X, (Hm X)^-1). + intros X Y f. simpl. use vcomp_move_R_Mp. { is_iso. } simpl. rewrite <- vassocr. use vcomp_move_L_pM. { is_iso. } symmetry. simpl. apply (modnaturality_of m). - use modification_eq. intro X. cbn. exact (vcomp_rinv (Hm X)). - use modification_eq. intro X. cbn. exact (vcomp_linv (Hm X)). 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.PrecategoryBinProduct. 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.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Identitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.Compositor. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.Transformations.PseudoTransformation.