Definition disp_iso_to_invetible_2cell_weq {a b : C} {f g : C⟦a,b⟧} {x : invertible_2cell f g} {aa : D a} {bb : D b} {ff : aa -->[ f ] bb} {gg : aa -->[ g ] bb} (xx : ff ==>[ x ] gg) : disp_iso_total xx ≃ @is_invertible_2cell (total_bicat D) (a ,, aa) (b ,, bb) (f ,, ff) (g ,, gg) (pr1 x ,, xx). Proof. exists (disp_iso_to_invetible_2cell xx). use isweq_iso. - apply disp_iso_to_invetible_2cell_inv. - intros z. use subtypePath. + intro; apply isapropdirprod ; apply (total_bicat D). + cbn. apply (transportf_set (λ z, gg ==>[ z ] ff)). apply C. - intros z. use subtypePath. + intro; apply isapropdirprod ; apply (total_bicat D). + use total2_paths_b. * cbn. exact (base_paths _ _ (pr1 (isaprop_is_invertible_2cell (pr1 x) (pr2 x) (pr1_invertible_2cell_total xx z)))). * cbn. reflexivity. 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.