Definition poset_to_bounded_lattice : bounded_lattice X. Proof. use make_bounded_lattice. - exact poset_to_lattice. - exact bot. - exact top. - exact poset_to_bounded_lattice_laws. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.