Definition make_bounded_lattice {X : hSet} {l : lattice X} {bot top : X} : bounded_latticeop l bot top → bounded_lattice X := λ bl, l,, bot,, top,, bl.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups. Require Import UniMath.OrderTheory.Lattice.Lattice.