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