Definition lattice_weq {X Y : hSet} (H : weq Y X) (lat : lattice X) : lattice Y. Proof. exists (binop_weq_bck H (Lmin lat)), (binop_weq_bck H (Lmax lat)). apply islatticeop_weq. apply (pr2 (pr2 lat)). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.