Definition sigma_idtoiso_2_0_alt (HD₁_2_0 : disp_univalent_2_0 D₁) (HD₂_2_0 : disp_univalent_2_0 D₂) {x : C} (xx yy : (sigma_bicat C D₁ D₂) x) : xx = yy ≃ disp_adjoint_equivalence (idtoiso_2_0 x x (idpath x)) xx yy. Proof. refine (_ ∘ total2_paths_equiv _ _ _)%weq. refine (pair_disp_adjequiv_to_sigma_disp_adjequiv_weq xx yy ∘ _)%weq. refine (weqtotal2 (make_weq _ (HD₁_2_0 x x (idpath _) (pr1 xx) (pr1 yy))) _)%weq. induction xx as [xx1 xx2]. induction yy as [yy1 yy2]. intro p ; cbn in p. induction p. unfold transportf ; simpl. refine (_ ∘ make_weq _ (HD₂_2_0 _ _ (idpath (x ,, xx1)) xx2 yy2))%weq. exact (disp_adjequiv_sigma_help_weq x xx1 xx2 yy2). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.