Lemma isaset_lattice (X : hSet) : isaset (lattice X) . Proof. use isaset_total2. - use (isasetbinoponhSet X). - intro min. use isaset_total2. -- use (isasetbinoponhSet X). -- intro max. use (isasetaprop (isaprop_islatticeop _ _)). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.