fact: Definition isinvbinophrel {X : setwithbinop} (R : hrel X) : UU := dirprod (∏ a b c : X, R (op c a) (op c b) -> R a b) (∏ a b c : X, R (op a c) (op b c) -> R a b).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions