Definition double_hor_comp_mor {C : category} {D : twosided_disp_cat C C} (Cm : hor_comp_data D) {x₁ x₂ y₁ y₂ z₁ z₂ : C} {v₁ : x₁ --> x₂} {v₂ : y₁ --> y₂} {v₃ : z₁ --> z₂} {h₁ : D x₁ y₁} {h₂ : D y₁ z₁} {k₁ : D x₂ y₂} {k₂ : D y₂ z₂} (s₁ : h₁ -->[ v₁ ][ v₂ ] k₁) (s₂ : h₂ -->[ v₂ ][ v₃ ] k₂) : double_hor_comp Cm h₁ h₂ -->[ v₁ ][ v₃ ] double_hor_comp Cm k₁ k₂ := pr2 Cm x₁ x₂ y₁ y₂ z₁ z₂ v₁ v₂ v₃ h₁ h₂ k₁ k₂ s₁ s₂.
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.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.