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