Definition hor_comp_laws {C : category} {D : twosided_disp_cat C C} (Cm : hor_comp_data D) : UU := (∏ (x y z : C) (h₁ : D x y) (h₂ : D y z), double_hor_comp_mor Cm (id_two_disp h₁) (id_two_disp h₂) = id_two_disp (double_hor_comp Cm h₁ h₂)) × (∏ (x₁ x₂ x₃ y₁ y₂ y₃ z₁ z₂ z₃ : C) (v₁ : x₁ --> x₂) (v₁' : x₂ --> x₃) (v₂ : y₁ --> y₂) (v₂' : y₂ --> y₃) (v₃ : z₁ --> z₂) (v₃' : z₂ --> z₃) (h₁ : D x₁ y₁) (h₂ : D y₁ z₁) (k₁ : D x₂ y₂) (k₂ : D y₂ z₂) (l₁ : D x₃ y₃) (l₂ : D y₃ z₃) (s₁ : h₁ -->[ v₁ ][ v₂ ] k₁) (s₁' : k₁ -->[ v₁' ][ v₂' ] l₁) (s₂ : h₂ -->[ v₂ ][ v₃ ] k₂) (s₂' : k₂ -->[ v₂' ][ v₃' ] l₂), double_hor_comp_mor Cm (s₁ ;;2 s₁') (s₂ ;;2 s₂') = double_hor_comp_mor Cm s₁ s₂ ;;2 double_hor_comp_mor Cm 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.