Definition disp_iso_to_invetible_2cell_inv {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) : @is_invertible_2cell (total_bicat D) (a ,, aa) (b ,, bb) (f ,, ff) (g ,, gg) (pr1 x ,, xx) → disp_iso_total xx. Proof. intros z. use tpair. - refine (transportb (λ z, _ ==>[ z ] _) _ (pr2 (pr1 z))). exact (base_paths _ _ (pr1 (isaprop_is_invertible_2cell (pr1 x) (pr2 x) (pr1_invertible_2cell_total xx z)))). - split ; cbn. + use total2_paths_b. * apply vcomp_rinv. * cbn. induction z as [inv Hz]. induction inv as [inv1 inv2]. induction Hz as [H1 H2]. cbn in H1, H2. pose (fiber_paths H1) as p. cbn in p. rewrite <- p ; clear p. rewrite transport_b_f. cbn. unfold transportb. rewrite (@disp_mor_transportf_prewhisker). apply (@transportf_paths _ (λ z, ff ==>[ z ] ff)). apply C. + use total2_paths_b. * apply vcomp_linv. * cbn. induction z as [inv Hz]. induction inv as [inv1 inv2]. induction Hz as [H1 H2]. cbn in H1, H2. pose (fiber_paths H2) as p. cbn in p. rewrite <- p ; clear p. rewrite transport_b_f. cbn. unfold transportb. rewrite (@disp_mor_transportf_postwhisker). apply (@transportf_paths _ (λ z, gg ==>[ z ] gg)). apply C. 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.