proposition: Lemma isabmonoidop_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) : isabmonoidop opp → isabmonoidop (binop_weq_fwd H opp).
proof: Proof. intro is. split. apply ismonoidop_weq_fwd, (pr1 is). apply iscomm_weq_fwd, (pr2 is). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions