proposition: Lemma step2 {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), ∑ (Hα : is_invertible_2cell α), is_disp_invertible_2cell Hα αα) ≃ (∑ (i : invertible_2cell f g), disp_invertible_2cell i ff gg).
proof: Proof. eapply weqcomp. 2: { apply weqtotal2asstol. } unfold disp_invertible_2cell. eapply weqfibtototal. intros α. cbn. apply weqtotal2comm. 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