Definition isdecrel_latticedec {X : hSet} (lat : latticedec X) : isdecrel (Lle lat) := pr2 (pr2 lat).
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.