Definition poset_to_lattice : lattice X. Proof. use make_lattice. - exact (min_op min). - exact (max_op max). - exact poset_to_lattice_laws. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.