Lemma isaset_prebilattice (X : hSet) : isaset (prebilattice X) . Proof. exact(isaset_dirprod (isaset_lattice X) (isaset_lattice X)). Defined.
Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.