Definition hor_op_twosided_disp_cat_id_comp : twosided_disp_cat_id_comp hor_op_twosided_disp_cat_ob_mor. Proof. split. - exact (λ y x xy, id_two_disp xy). - exact (λ y₁ y₂ y₃ x₁ x₂ x₃ xy₁ xy₂ xy₃ g₁ g₂ f₁ f₂ fg₁ fg₂, 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.