proposition: Lemma step1 {x y : C} {xx : D x} {yy : D y} {f g : C⟦x,y⟧} {ff : xx -->[ f ] yy} {gg : xx -->[ g ] yy} : @invertible_2cell E (x ,, xx) (y ,, yy) (f,, ff) (g,, gg) ≃ (∑ (α : f ==> g) (αα : ff ==>[α] gg), ∑ (Hα : is_invertible_2cell α), is_disp_invertible_2cell Hα αα).
proof: Proof. eapply weqcomp. { apply weqfibtototal. intro. apply is_invertible_total_to_disp_weq. } eapply weqcomp. { apply weqinvweq. apply weqtotal2asstol. } apply idweq. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.Invertible_2cells