proposition: Proposition double_hor_comp_mor_comp {C : category} {D : twosided_disp_cat C C} (Cm : hor_comp D) {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₂'.
proof: Proof. exact ((pr22 Cm) x₁ x₂ x₃ y₁ y₂ y₃ z₁ z₂ z₃ v₁ v₁' v₂ v₂' v₃ v₃' h₁ h₂ k₁ k₂ l₁ l₂ s₁ s₁' s₂ s₂'). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos