Definition disp_isotoid_idtoiso_2_1 {B : bicat} {D : disp_bicat B} (HD_2_1 : disp_univalent_2_1 D) {b₁ b₂ : B} {f g : b₁ --> b₂} (p : f = g) {bb₁ : D b₁} {bb₂ : D b₂} {ff : bb₁ -->[ f ] bb₂} {gg : bb₁ -->[ g ] bb₂} (pp : transportf (λ z, bb₁ -->[ z] bb₂) p ff = gg) : disp_isotoid_2_1 _ HD_2_1 p ff gg (disp_idtoiso_2_1 _ p ff gg pp) = pp. Proof. exact (homotinvweqweq (make_weq _ (HD_2_1 b₁ b₂ f g p bb₁ bb₂ ff gg)) pp). Qed. Section Total_Category_Univalent_2_1. Context {C : bicat}. Variable (D : disp_bicat C) (HC : is_univalent_2_1 C) (HD : disp_univalent_2_1 D). Local Definition E := (total_bicat D). Local Definition path_E {x y : C} {xx : D x} {yy : D y} {f g : C⟦x,y⟧} (ff : xx -->[ f ] yy) (gg : xx -->[ g ] yy) : (f,, ff = g,, gg) ≃ ∑ (p : f = g), transportf _ p ff = gg := total2_paths_equiv _ (f ,, ff) (g ,, gg). Local Definition path_to_iso_E {x y : C} {xx : D x} {yy : D y} {f g : C⟦x,y⟧} (ff : xx -->[ f ] yy) (gg : xx -->[ g ] yy) : (∑ (p : f = g), transportf _ p ff = gg) ≃ ∑ (i : invertible_2cell f g), disp_invertible_2cell i ff gg. Proof. use weqbandf. - exact (idtoiso_2_1 f g ,, HC x y f g). - cbn. intros p. exact (disp_idtoiso_2_1 D p ff gg ,, HD x y f g p xx yy ff gg). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.