Definition disp_iso_to_invetible_2cell {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. intros z. use tpair. - use tpair. + exact (x^-1). + exact (pr1 z). - split ; cbn. + use total2_paths_f ; cbn. * apply vcomp_rinv. * refine (_ @ fiber_paths (pr1 (pr2 z))) ; cbn. apply (@transportf_paths _ (λ α : f ==> f, ff ==>[ α] ff)). apply C. + use total2_paths_f ; cbn. * apply vcomp_linv. * refine (_ @ fiber_paths (pr2 (pr2 z))) ; cbn. apply (@transportf_paths _ (λ α : g ==> g, gg ==>[ α] 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.