Lemma isassoc_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) : isassoc opp → isassoc (binop_weq_fwd H opp). Proof. intros is x y z. apply (maponpaths H). refine (_ @ is _ _ _ @ _). - apply (maponpaths (λ x, opp x _)). apply homotinvweqweq. - apply maponpaths. apply homotinvweqweq0. Defined.