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.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.