Definition latticedec_weq {X Y : hSet} (H : weq Y X) : latticedec X → latticedec Y. Proof. intros lat. exists (lattice_weq H (lattice_latticedec lat)). split. - apply istotal_Lle_weq. apply istotal_latticedec. - apply isdecrel_Lle_weq. apply isdecrel_latticedec. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.