Definition is_invertible_total_to_fiber {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) : forall (Hαα: @is_invertible_2cell E (x ,, xx) (y ,, yy) (f,, ff) (g,, gg) (α,,αα)), is_disp_invertible_2cell (is_invertible_total_to_base _ _ Hαα) αα. Proof. intros Hz. induction Hz as [inv Hz]. induction inv as [i ii]. induction Hz as [Hz1 Hz2]. cbn in *. use tpair. - exact ii. - cbn. split. * apply (@transportf_transpose_right _ (λ α : f ==> f, ff ==>[ α] ff)). refine (_ @ fiber_paths Hz1). apply (@transportf_paths _ (λ α : f ==> f, ff ==>[ α] ff)). apply pathsinv0inv0. * apply (@transportf_transpose_right _ (λ α : g ==> g, gg ==>[ α] gg)). refine (_ @ fiber_paths Hz2). apply (@transportf_paths _ (λ α : g ==> g, gg ==>[ α] gg)). apply pathsinv0inv0. 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.