proposition: Lemma compeq {C : category} {x y z : C} {f f' : x --> y} {g g' : y --> z} : f = f' -> g = g' -> f · g = f' · g'.
proof: Proof. intros Hf Hg. induction Hf. induction Hg. reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three