Definition lattice_latticewithgt {X : hSet} : latticewithgt X → lattice X := pr1.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.