Definition is_invertible_disp_to_total {x y : C} {xx : D x} {yy : D y} {f g : C⟦x,y⟧} {ff : xx -->[ f ] yy} {gg : xx -->[ g ] yy} (α : f ==> g) (αα : ff ==>[α] gg) : (∑ (Hα : is_invertible_2cell α), is_disp_invertible_2cell Hα αα) → (@is_invertible_2cell E (x ,, xx) (y ,, yy) (f,, ff) (g,, gg) (α,,αα)). Proof. intros H. pose (Hα := pr1 H). pose (Hαα := pr2 H). cbn in Hαα. pose (αα' := (αα,,Hαα) : disp_invertible_2cell (α,,Hα) _ _). use tpair. - use tpair. + exact (inv_cell Hα). + exact (disp_inv_cell αα'). - split. + cbn. use total2_paths_b. ** apply vcomp_rinv. ** apply (disp_vcomp_rinv αα'). + cbn. use total2_paths_b. ** apply vcomp_linv. ** apply (disp_vcomp_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.