Definition bot {X: hSet} (b : bounded_prebilattice X) : X := Lbot (pr2 b) .
Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.