proposition: 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: Proof. intros is x y. unfold binop_weq_bck. refine (pathscomp0 _ (homotinvweqweq H _)). apply maponpaths. refine (pathscomp0 _ (is _ _)). apply maponpaths. apply (homotweqinvweq H). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions