------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles for order-theoretic lattices
------------------------------------------------------------------------
 
-- The contents of this module should be accessed via
-- `Relation.Binary.Lattice`.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Relation.Binary.Lattice.Bundles where
 
open import Algebra.Core
open import Level using (suc; _⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Poset; Setoid)
open import Relation.Binary.Lattice.Structures
 
------------------------------------------------------------------------
-- Join semilattices
 
record JoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∨_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_               : Rel Carrier ℓ₂  -- The partial order.
    _∨_               : Op₂ Carrier     -- The join operation.
    isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
 
  open IsJoinSemilattice isJoinSemilattice public
 
  poset : Poset c ℓ₁ ℓ₂
  poset = record { isPartialOrder = isPartialOrder }
 
  open Poset poset public using (preorder)
 
 
record BoundedJoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∨_
  field
    Carrier                  : Set c
    _≈_                      : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_                      : Rel Carrier ℓ₂  -- The partial order.
    _∨_                      : Op₂ Carrier     -- The join operation.
    ⊥                        : Carrier         -- The minimum.
    isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥
 
  open IsBoundedJoinSemilattice isBoundedJoinSemilattice public
 
  joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
  joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }
 
  open JoinSemilattice joinSemilattice public using (preorder; poset)
 
------------------------------------------------------------------------
-- Meet semilattices
 
record MeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∧_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_               : Rel Carrier ℓ₂  -- The partial order.
    _∧_               : Op₂ Carrier     -- The meet operation.
    isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
 
  open IsMeetSemilattice isMeetSemilattice public
 
  poset : Poset c ℓ₁ ℓ₂
  poset = record { isPartialOrder = isPartialOrder }
 
  open Poset poset public using (preorder)
 
record BoundedMeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∧_
  field
    Carrier                  : Set c
    _≈_                      : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_                      : Rel Carrier ℓ₂  -- The partial order.
    _∧_                      : Op₂ Carrier     -- The join operation.
    ⊤                        : Carrier         -- The maximum.
    isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤
 
  open IsBoundedMeetSemilattice isBoundedMeetSemilattice public
 
  meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
  meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }
 
  open MeetSemilattice meetSemilattice public using (preorder; poset)
 
------------------------------------------------------------------------
-- Lattices
 
record Lattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∨_
  infixr  _∧_
  field
    Carrier   : Set c
    _≈_       : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_       : Rel Carrier ℓ₂  -- The partial order.
    _∨_       : Op₂ Carrier     -- The join operation.
    _∧_       : Op₂ Carrier     -- The meet operation.
    isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
 
  open IsLattice isLattice public
 
  setoid : Setoid c ℓ₁
  setoid = record { isEquivalence = isEquivalence }
 
  joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
  joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }
 
  meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
  meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }
 
  open JoinSemilattice joinSemilattice public using (poset; preorder)
 
record DistributiveLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∨_
  infixr  _∧_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_     : Rel Carrier ℓ₂  -- The partial order.
    _∨_     : Op₂ Carrier     -- The join operation.
    _∧_     : Op₂ Carrier     -- The meet operation.
    isDistributiveLattice : IsDistributiveLattice _≈_ _≤_ _∨_ _∧_
 
  open IsDistributiveLattice isDistributiveLattice using (∧-distribˡ-∨) public
  open IsDistributiveLattice isDistributiveLattice using (isLattice)
 
  lattice : Lattice c ℓ₁ ℓ₂
  lattice = record { isLattice = isLattice }
 
  open Lattice lattice hiding (Carrier; _≈_; _≤_; _∨_; _∧_) public
 
record BoundedLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∨_
  infixr  _∧_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_              : Rel Carrier ℓ₂  -- The partial order.
    _∨_              : Op₂ Carrier     -- The join operation.
    _∧_              : Op₂ Carrier     -- The meet operation.
    ⊤                : Carrier         -- The maximum.
    ⊥                : Carrier         -- The minimum.
    isBoundedLattice : IsBoundedLattice _≈_ _≤_ _∨_ _∧_ ⊤ ⊥
 
  open IsBoundedLattice isBoundedLattice public
 
  boundedJoinSemilattice : BoundedJoinSemilattice c ℓ₁ ℓ₂
  boundedJoinSemilattice = record
    { isBoundedJoinSemilattice = isBoundedJoinSemilattice }
 
  boundedMeetSemilattice : BoundedMeetSemilattice c ℓ₁ ℓ₂
  boundedMeetSemilattice = record
    { isBoundedMeetSemilattice = isBoundedMeetSemilattice }
 
  lattice : Lattice c ℓ₁ ℓ₂
  lattice = record { isLattice = isLattice }
 
  open Lattice lattice public
    using (joinSemilattice; meetSemilattice; poset; preorder; setoid)
 
------------------------------------------------------------------------
-- Heyting algebras (a bounded lattice with exponential operator)
 
record HeytingAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _⇨_
  infixr  _∨_
  infixr  _∧_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_              : Rel Carrier ℓ₂  -- The partial order.
    _∨_              : Op₂ Carrier     -- The join operation.
    _∧_              : Op₂ Carrier     -- The meet operation.
    _⇨_              : Op₂ Carrier     -- The exponential operation.
    ⊤                : Carrier         -- The maximum.
    ⊥                : Carrier         -- The minimum.
    isHeytingAlgebra : IsHeytingAlgebra _≈_ _≤_ _∨_ _∧_ _⇨_ ⊤ ⊥
 
  boundedLattice : BoundedLattice c ℓ₁ ℓ₂
  boundedLattice = record
    { isBoundedLattice = IsHeytingAlgebra.isBoundedLattice isHeytingAlgebra }
 
  open IsHeytingAlgebra isHeytingAlgebra
    using (exponential; transpose-⇨; transpose-∧) public
  open BoundedLattice boundedLattice
    hiding (Carrier; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥) public
 
------------------------------------------------------------------------
-- Boolean algebras (a specialized Heyting algebra)
 
record BooleanAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix   _≈_ _≤_
  infixr  _∨_
  infixr  _∧_
  infix  ¬_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_              : Rel Carrier ℓ₂  -- The partial order.
    _∨_              : Op₂ Carrier     -- The join operation.
    _∧_              : Op₂ Carrier     -- The meet operation.
    ¬_               : Op₁ Carrier     -- The negation operation.
    ⊤                : Carrier         -- The maximum.
    ⊥                : Carrier         -- The minimum.
    isBooleanAlgebra : IsBooleanAlgebra _≈_ _≤_ _∨_ _∧_ ¬_ ⊤ ⊥
 
  open IsBooleanAlgebra isBooleanAlgebra using (isHeytingAlgebra)
 
  heytingAlgebra : HeytingAlgebra c ℓ₁ ℓ₂
  heytingAlgebra = record { isHeytingAlgebra = isHeytingAlgebra }
 
  open HeytingAlgebra heytingAlgebra public
    hiding (Carrier; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥)