proposition: Lemma iscomp2binoptransrel {X : setwith2binop} (R : hrel X) (is : istrans R) (isb : is2binophrel R) : dirprod (iscomprelrelfun2 R R (@op1 X)) (iscomprelrelfun2 R R (@op2 X)).
proof: Proof. split. - apply (@iscompbinoptransrel (setwithbinop1 X) R is (pr1 isb)). - apply (@iscompbinoptransrel (setwithbinop2 X) R is (pr2 isb)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions