Definition vcomp_disp_is_invertible : is_disp_invertible_2cell (comp_of_invertible_2cell α β) (αα •• ββ). Proof. use tpair. - exact (disp_inv_cell ββ •• disp_inv_cell αα). - split. + exact vcomp_disp_is_invertible_rinv. + exact vcomp_disp_is_invertible_linv. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Invertible_2cells.