Lemma isabsorb_weq_fwd {X Y : UU} (H : X ≃ Y) (op1 op2 : binop X) : isabsorb op1 op2 → isabsorb (binop_weq_fwd H op1) (binop_weq_fwd H op2). Proof. intros is x y. unfold binop_weq_fwd. refine (_ @ homotweqinvweq H _). apply maponpaths. refine (_ @ is _ _). apply maponpaths. apply (homotinvweqweq H). Defined.