fact: Definition iscommringopsisof {X Y : setwith2binop} (f : twobinopiso X Y) (is : iscommringops (@op1 X) (@op2 X)) : iscommringops (@op1 Y) (@op2 Y) := make_dirprod (isringopsisof f is) (iscommisof (binop2iso f) (pr2 is)).
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions