Lemma isassoc_weq_bck {X Y : UU} (H : X ≃ Y) (opp : binop Y) : isassoc opp → isassoc (binop_weq_bck H opp). Proof. intros is x y z. apply (maponpaths (invmap H)). refine (_ @ is _ _ _ @ _). - apply (maponpaths (λ x, opp x _)). apply homotweqinvweq. - apply maponpaths. symmetry. apply homotweqinvweq. Defined.