Definition is_invertible_total_to_base {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) : @is_invertible_2cell E (x ,, xx) (y ,, yy) (f,, ff) (g,, gg) (α,,αα) → is_invertible_2cell α. Proof. intros Hz. induction Hz as [inv Hz]. induction inv as [i ii]. induction Hz as [Hz1 Hz2]. cbn in *. use tpair. - exact i. - cbn. split. + exact (base_paths _ _ Hz1). + exact (base_paths _ _ Hz2). 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.