Definition ver_op_twosided_disp_cat_id_comp : twosided_disp_cat_id_comp ver_op_twosided_disp_cat_ob_mor. Proof. split. - exact (λ (x : C₁) (y : C₂) (xy : D x y), id_two_disp xy). - exact (λ (x₁ x₂ x₃ : C₁) (y₁ y₂ y₃ : C₂) (xy₁ : D x₁ y₁) (xy₂ : D x₂ y₂) (xy₃ : D x₃ y₃) (f₁ : x₂ --> x₁) (f₂ : x₃ --> x₂) (g₁ : y₂ --> y₁) (g₂ : y₃ --> y₂) (fg₁ : xy₂ -->[ f₁ ][ g₁ ] xy₁) (fg₂ : xy₃ -->[ f₂ ][ g₂ ] xy₂), fg₂ ;;2 fg₁). 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.