Definition mor_cong_rel_to_eqrel {C : category} (eq : mor_cong_rel C) {x y : C} (f g : x --> y) : hProp := pr1 eq x y f g.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude.