Definition bounded_prebilattice (X : hSet) := bounded_lattice X × bounded_lattice X.
Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.