Definition iso_ver_op_twosided_disp_cat_weq {x : C₁} {y : C₂} (xy₁ xy₂ : D x y) : iso_twosided_disp (D := D) (identity_z_iso _) (identity_z_iso _) xy₁ xy₂ ≃ iso_twosided_disp (D := ver_op_twosided_disp_cat) (identity_z_iso _) (identity_z_iso _) xy₂ xy₁. Proof. use weqfibtototal. intros fg. use weqimplimpl. - apply to_iso_ver_op_twosided_disp_cat. - apply from_iso_ver_op_twosided_disp_cat. - apply isaprop_is_iso_twosided_disp. - apply isaprop_is_iso_twosided_disp. 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.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness.