Definition isLattice {X:hSet} (le:hrel X) (min max:binop X) := ∑ po : isPartialOrder le, ∑ lub : ∏ x y z, le x z ∧ le y z <-> le (max x y) z, ∑ glb : ∏ x y t, le t x ∧ le t y <-> le t (min x y), unit.
Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.OrderTheory.Posets.Examples.StandardFiniteSet.