module Lattice where

open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import Data.Nat using (ℕ; _≤_)
open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym)
open import Agda.Primitive using (lsuc)

record Preorder {a} (A : Set a) : Set (lsuc a) where
    field
        _≼_ : A → A → Set a

        ≼-refl : Reflexive (_≼_)
        ≼-trans : Transitive (_≼_)
        ≼-antisym : Antisymmetric (_≡_) (_≼_)

record Semilattice {a} (A : Set a) : Set (lsuc a) where
    field
        _⊔_ : A → A → A

        ⊔-assoc : (x : A) → (y : A) → (z : A) → x ⊔ (y ⊔ z) ≡ (x ⊔ y) ⊔ z
        ⊔-comm : (x : A) → (y : A) → x ⊔ y ≡ y ⊔ x
        ⊔-idemp : (x : A) → x ⊔ x ≡ x

record Lattice {a} (A : Set a) : Set (lsuc a) where
    field
        joinSemilattice : Semilattice A
        meetSemilattice : Semilattice A

    _⊔_ = Semilattice._⊔_ joinSemilattice
    _⊓_ = Semilattice._⊔_ meetSemilattice

    field
        absorb-⊔-⊓ : (x : A) → (y : A) → x ⊔ (x ⊓ y) ≡ x
        absorb-⊓-⊔ : (x : A) → (y : A) → x ⊓ (x ⊔ y) ≡ x

instance
    NatPreorder : Preorder ℕ
    NatPreorder = record { _≼_ = _≤_; ≼-refl = ≤-refl; ≼-trans = ≤-trans; ≼-antisym = ≤-antisym }