------------------------------------------------------------------------
-- The Agda standard library
--
-- Structures for order-theoretic lattices
------------------------------------------------------------------------

-- The contents of this module should be accessed via
-- `Relation.Binary.Lattice`.

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsPartialOrder)
open import Relation.Binary.Definitions using (Minimum; Maximum)

module Relation.Binary.Lattice.Structures
 {a ℓ₁ ℓ₂} {A : Set a}
 (_≈_ : Rel A ℓ₁) -- The underlying equality.
 (_≤_ : Rel A ℓ₂) -- The partial order.
 where

open import Algebra.Core
open import Algebra.Definitions
open import Data.Product.Base using (_×_; _,_)
open import Level using (suc; _⊔_)

open import Relation.Binary.Lattice.Definitions

------------------------------------------------------------------------
-- Join semilattices

record IsJoinSemilattice (_∨_ : Op₂ A)    -- The join operation.
                         : Set (a  ℓ₁  ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    supremum       : Supremum _≤_ _∨_

  x≤x∨y :  x y  x  (x  y)
  x≤x∨y x y = let pf , _ , _ = supremum x y in pf

  y≤x∨y :  x y  y  (x  y)
  y≤x∨y x y = let _ , pf , _ = supremum x y in pf

  ∨-least :  {x y z}  x  z  y  z  (x  y)  z
  ∨-least {x} {y} {z} = let _ , _ , pf = supremum x y in pf z

  open IsPartialOrder isPartialOrder public

record IsBoundedJoinSemilattice (_∨_ : Op₂ A)    -- The join operation.
                                (   : A)        -- The minimum.
                                : Set (a  ℓ₁  ℓ₂) where
  field
    isJoinSemilattice : IsJoinSemilattice _∨_
    minimum           : Minimum _≤_ 

  open IsJoinSemilattice isJoinSemilattice public

------------------------------------------------------------------------
-- Meet semilattices

record IsMeetSemilattice (_∧_ : Op₂ A)    -- The meet operation.
                         : Set (a  ℓ₁  ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    infimum        : Infimum _≤_ _∧_

  x∧y≤x :  x y  (x  y)  x
  x∧y≤x x y = let pf , _ , _ = infimum x y in pf

  x∧y≤y :  x y  (x  y)  y
  x∧y≤y x y = let _ , pf , _ = infimum x y in pf

  ∧-greatest :  {x y z}  x  y  x  z  x  (y  z)
  ∧-greatest {x} {y} {z} = let _ , _ , pf = infimum y z in pf x

  open IsPartialOrder isPartialOrder public

record IsBoundedMeetSemilattice (_∧_ : Op₂ A)    -- The join operation.
                                (   : A)        -- The maximum.
                                : Set (a  ℓ₁  ℓ₂) where
  field
    isMeetSemilattice : IsMeetSemilattice _∧_
    maximum           : Maximum _≤_ 

  open IsMeetSemilattice isMeetSemilattice public

------------------------------------------------------------------------
-- Lattices

record IsLattice (_∨_ : Op₂ A)    -- The join operation.
                 (_∧_ : Op₂ A)    -- The meet operation.
                 : Set (a  ℓ₁  ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    supremum       : Supremum _≤_ _∨_
    infimum        : Infimum _≤_ _∧_

  isJoinSemilattice : IsJoinSemilattice  _∨_
  isJoinSemilattice = record
    { isPartialOrder = isPartialOrder
    ; supremum       = supremum
    }

  isMeetSemilattice : IsMeetSemilattice  _∧_
  isMeetSemilattice = record
    { isPartialOrder = isPartialOrder
    ; infimum        = infimum
    }

  open IsJoinSemilattice isJoinSemilattice public
    using (x≤x∨y; y≤x∨y; ∨-least)
  open IsMeetSemilattice isMeetSemilattice public
    using (x∧y≤x; x∧y≤y; ∧-greatest)
  open IsPartialOrder isPartialOrder public

record IsDistributiveLattice (_∨_ : Op₂ A)    -- The join operation.
                             (_∧_ : Op₂ A)    -- The meet operation.
                             : Set (a  ℓ₁  ℓ₂) where
  field
    isLattice    : IsLattice _∨_ _∧_
    ∧-distribˡ-∨ : _DistributesOverˡ_ _≈_ _∧_ _∨_

  open IsLattice isLattice public

record IsBoundedLattice (_∨_ : Op₂ A)    -- The join operation.
                        (_∧_ : Op₂ A)    -- The meet operation.
                        (   : A)        -- The maximum.
                        (   : A)        -- The minimum.
                        : Set (a  ℓ₁  ℓ₂) where
  field
    isLattice : IsLattice _∨_ _∧_
    maximum   : Maximum _≤_ 
    minimum   : Minimum _≤_ 

  open IsLattice isLattice public

  isBoundedJoinSemilattice : IsBoundedJoinSemilattice  _∨_ 
  isBoundedJoinSemilattice = record
    { isJoinSemilattice = isJoinSemilattice
    ; minimum           = minimum
    }

  isBoundedMeetSemilattice : IsBoundedMeetSemilattice _∧_ 
  isBoundedMeetSemilattice = record
    { isMeetSemilattice = isMeetSemilattice
    ; maximum           = maximum
    }

------------------------------------------------------------------------
-- Heyting algebras (a bounded lattice with exponential operator)

record IsHeytingAlgebra (_∨_ : Op₂ A)    -- The join operation.
                        (_∧_ : Op₂ A)    -- The meet operation.
                        (_⇨_ : Op₂ A)    -- The exponential operation.
                        (   : A)        -- The maximum.
                        (   : A)        -- The minimum.
                        : Set (a  ℓ₁  ℓ₂) where
  field
    isBoundedLattice : IsBoundedLattice _∨_ _∧_  
    exponential      : Exponential _≤_ _∧_ _⇨_

  transpose-⇨ :  {w x y}  (w  x)  y  w  (x  y)
  transpose-⇨ {w} {x} {y} = let pf , _ = exponential w x y in pf

  transpose-∧ :  {w x y}  w  (x  y)  (w  x)  y
  transpose-∧ {w} {x} {y} = let _ , pf = exponential w x y in pf

  open IsBoundedLattice isBoundedLattice public

------------------------------------------------------------------------
-- Boolean algebras (a specialized Heyting algebra)

record IsBooleanAlgebra (_∨_ : Op₂ A)    -- The join operation.
                        (_∧_ : Op₂ A)    -- The meet operation.
                        (¬_ : Op₁ A)     -- The negation operation.
                        (   : A)        -- The maximum.
                        (   : A)        -- The minimum.
                        : Set (a  ℓ₁  ℓ₂) where
  infixr 5 _⇨_
  _⇨_ : Op₂ A
  x  y = (¬ x)  y

  field
    isHeytingAlgebra : IsHeytingAlgebra _∨_ _∧_ _⇨_  

  open IsHeytingAlgebra isHeytingAlgebra public