Definition iso_twosided_disp_two_cat_arrow_weq {x y : C} (f g : two_cat_arrow_twosided_disp_cat x y) : z_iso (C := hom_cat x y) f g ≃ iso_twosided_disp (identity_z_iso x) (identity_z_iso y) f g. Proof. use weq_iso. - exact z_iso_to_iso_two_cat_arrow. - exact iso_two_cat_arrow_to_z_iso. - apply iso_twosided_disp_two_cat_arrow_weq_left. - apply iso_twosided_disp_two_cat_arrow_weq_right. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.TwoCategories. Import TwoCategories.Notations. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Total. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete.