Definition make_mor_cong_rel {C : category} (eq : ∏ (x y : C), eqrel (x --> y)) (eqc : ∏ (x y z : C) (f f' : x --> y) (g g' : y --> z), eq _ _ f f' → eq _ _ g g' → eq _ _ (f · g) (f' · g')) : mor_cong_rel C := eq ,, eqc.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude.