Definition disp_vcomp_linv {α : invertible_2cell f f'} {ff : d -->[f] d'} {ff' : d -->[f'] d'} (e : disp_invertible_2cell α ff ff') : disp_inv_cell e •• e = transportb (λ α, _ ==>[α] _) (vcomp_linv α) (disp_id2 ff') := pr2 (pr2 (pr2 e)).
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.