Definition iso_twosided_disp_cat_on_disp_cat_weq {x : E₁} {y : E₂} (xy₁ xy₂ : twosided_disp_cat_on_disp_cat x y) : iso_twosided_disp (identity_z_iso (pr1 x)) (identity_z_iso (pr1 y)) xy₁ xy₂ ≃ iso_twosided_disp (identity_z_iso x) (identity_z_iso y) xy₁ xy₂. Proof. use weq_iso. - apply to_iso_twosided_disp_cat_on_disp_cat. - apply from_iso_twosided_disp_cat_on_disp_cat. - abstract (intro fg ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; apply idpath). - abstract (intro fg ; use subtypePath ; [ intro ; apply isaprop_is_iso_twosided_disp | ] ; apply idpath). 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.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total.