Definition max_el (X : Poset) : UU := ∑ (x : X), ∏ (y : X), y ≤ x. Coercion max_el_to_el {X : Poset} (m : max_el X) : X. Proof. exact (pr1 m). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.