proposition: Lemma binophrelandfun {X Y : setwithbinop} (f : binopfun X Y) (R : hrel Y) (is : @isbinophrel Y R) : @isbinophrel X (λ x x', R (f x) (f x')).
proof: Proof. set (ish := (pr2 f) : ∏ a0 b0, paths (f (op a0 b0)) (op (f a0) (f b0))). split. - intros a b c r. rewrite (ish _ _). rewrite (ish _ _). apply (pr1 is). apply r. - intros a b c r. rewrite (ish _ _). rewrite (ish _ _). apply (pr2 is). apply r. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions