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