Definition two_cat_arrow_twosided_disp_cat_id_comp : twosided_disp_cat_id_comp two_cat_arrow_twosided_disp_cat_ob_mor. Proof. split. - intros x y xy ; cbn. exact (two_cat_runitor _ • two_cat_linvunitor _). - intros x₁ x₂ x₃ y₁ y₂ y₃ xy₁ xy₂ xy₃ f₁ f₂ g₁ g₂ τ θ ; cbn in *. exact (two_cat_lassociator _ _ _ • (τ ▹ _) • two_cat_rassociator _ _ _ • (_ ◃ θ) • two_cat_lassociator _ _ _). 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.