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. eapply weqcomp. 2: { apply weqtotal2asstol. } unfold disp_invertible_2cell. eapply weqfibtototal. intros α. cbn. apply weqtotal2comm. 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.