Definition is_disp_invertible_2cell' {α : invertible_2cell f f'} {ff : d -->[f] d'} {ff' : d -->[f'] d'} (x : ff ==>[α] ff') : UU := ∑ (y : ff' ==>[α^-1] ff), (x •• y = transportb (λ α, _ ==>[α] _) (vcomp_rinv α) (disp_id2 ff)) × (y •• x = transportb (λ α, _ ==>[α] _) (vcomp_linv α) (disp_id2 ff')).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. 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.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence.