Definition max_operation (X : Poset) : UU := ∏ (x y : X), ∑ (m : X), x ≤ m × y ≤ m × ∏ (z : X), x ≤ z → y ≤ z → m ≤ z.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.