Definition ver_sq_compose {C : predoublecategory_sq_hor_ver_data} { a0 a1 b0 b1 c0 c1 : C } {f0: a0 -h-> a1} {f1: b0 -h-> b1} {f2: c0 -h-> c1} {g0: a0 -v-> b0} {h0: b0 -v-> c0} {g1: a1 -v-> b1} {h1: b1 -v-> c1} : (sqq f0 g0 g1 f1) → (sqq f1 h0 h1 f2) → (sqq f0 (g0 ·v h0) (g1 ·v h1) f2) := 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.