fact: Definition hor_sq_compose {C : predoublecategory_sq_hor_data} { a0 a1 b0 b1 c0 c1 : C } {f0: a0 -v-> a1} {f1: b0 -v-> b1} {f2: c0 -v-> c1} {g0: a0 -h-> b0} {h0: b0 -h-> c0} {g1: a1 -h-> b1} {h1: b1 -h-> c1} : (sqq g0 f0 f1 g1) → (sqq h0 f1 f2 h1) → (sqq (g0 ·h h0) f0 f2 (g1 ·h h1)) := pr2 (pr2 C) a0 a1 b0 b1 c0 c1 f0 f1 f2 g0 h0 g1 h1.
imports: UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence