Definition iso_in_E_weq {x y : C} {xx : D x} {yy : D y} {f g : C⟦x,y⟧} (ff : xx -->[ f ] yy) (gg : xx -->[ g ] yy) : (∑ (i : invertible_2cell f g), disp_invertible_2cell i ff gg) ≃ (@invertible_2cell E (x ,, xx) (y ,, yy) (f,, ff) (g,, gg)). Proof. apply weqinvweq. eapply weqcomp. - apply step1. - apply step2. 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.