Proposition mor_cong_rel_congruence {C : category} {eq : mor_cong_rel C} {x y z : C} {f f' : x --> y} {g g' : y --> z} (p : f ~_{eq} f') (q : g ~_{eq} g') : f · g ~_{eq} f' · g'. Proof. exact (pr2 eq _ _ _ _ _ _ _ p q). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude.