Definition isrigops {X : UU} (opp1 opp2 : binop X) : UU := (∑ axs : (isabmonoidop opp1) × (ismonoidop opp2), (∏ x : X, opp2 (unel_is (pr1 axs)) x = unel_is (pr1 axs)) × (∏ x : X, opp2 x (unel_is (pr1 axs)) = unel_is (pr1 axs))) × (isdistr opp1 opp2).