Definition isrigopsisof {X Y : setwith2binop} (f : twobinopiso X Y) (is : isrigops (@op1 X) (@op2 X)) : isrigops (@op1 Y) (@op2 Y). Proof. split. - exists (isabmonoidopisof (binop1iso f) (rigop1axs_is is) ,, ismonoidopisof (binop2iso f) (rigop2axs_is is)). simpl. change (unel_is (ismonoidopisof (binop1iso f) (rigop1axs_is is))) with ((pr1 f) (rigunel1_is is)). split. + intro y. rewrite <- (homotweqinvweq f y). rewrite <- ((pr2 (pr2 f)) _ _). apply (maponpaths (pr1 f)). apply (rigmult0x_is is). + intro y. rewrite <- (homotweqinvweq f y). rewrite <- ((pr2 (pr2 f)) _ _). apply (maponpaths (pr1 f)). apply (rigmultx0_is is). - apply (isdistrisof f). apply (rigdistraxs_is is). Defined.