Definition all_disp_mor_iso {C₁ C₂ : category} (D : twosided_disp_cat C₁ C₂) : UU := ∏ (x₁ x₂ : C₁) (y₁ y₂ : C₂) (xy₁ : D x₁ y₁) (xy₂ : D x₂ y₂) (f : x₁ --> x₂) (g : y₁ --> y₂) (Hf : is_z_isomorphism f) (Hg : is_z_isomorphism g) (fg : xy₁ -->[ f ][ g ] xy₂), is_iso_twosided_disp Hf Hg fg.
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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.