Definition lattice_latticedec {X : hSet} (lat : latticedec X) : lattice X := pr1 lat.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.