Definition is_least_upperbound_lattice {X : hSet} (L : lattice X) {I : UU} (f : I → X) (x : X) : UU := is_upperbound_lattice L f x × ∏ (y : X), is_upperbound_lattice L f y → Lle L x y.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting.