Definition is_univalent_twosided_disp_cat {C₁ C₂ : category} (D : twosided_disp_cat C₁ C₂) : UU := ∏ (x₁ x₂ : C₁) (y₁ y₂ : C₂) (p : x₁ = x₂) (q : y₁ = y₂) (xy₁ : D x₁ y₁) (xy₂ : D x₂ y₂), isweq (idtoiso_twosided_disp p q (xy₁ := xy₁) (xy₂ := xy₂)).
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.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.