proposition: Lemma isassoc_weq_fwd {X Y : UU} (H : X ≃ Y) (opp : binop X) : isassoc opp → isassoc (binop_weq_fwd H opp).
proof: Proof. intros is x y z. apply (maponpaths H). refine (pathscomp0 _ (pathscomp0 (is _ _ _) _)). - apply (maponpaths (λ x, opp x _)). apply homotinvweqweq. - apply maponpaths. apply homotinvweqweq0. Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions