Lemma isapropisrigops {X : hSet} (opp1 opp2 : binop X) : isaprop (isrigops opp1 opp2). Proof. apply (isofhleveldirprod 1). - apply (isofhleveltotal2 1). + apply (isofhleveldirprod 1). * apply isapropisabmonoidop. * apply isapropismonoidop. + intro x. apply (isofhleveldirprod 1). * apply impred. intro x'. apply (setproperty X). * apply impred. intro x'. apply (setproperty X). - apply isapropisdistr. Defined.