    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Definitions of algebraic structures like semilattices and lattices
    -- (packed in records together with sets, operations, etc.), defined via
    -- meet/join operations and their properties
    --
    -- For lattices defined via an order relation, see
    -- Relation.Binary.Lattice.
    ------------------------------------------------------------------------

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

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

    module Algebra.Lattice.Bundles where

    open import Algebra.Core using (Op₁; Op₂)
    open import Algebra.Bundles using (Band)
    import Algebra.Lattice.Bundles.Raw as Raw
    open import Algebra.Lattice.Structures
      using ( IsSemilattice; IsMeetSemilattice; IsJoinSemilattice
            ; IsBoundedSemilattice; IsBoundedMeetSemilattice
            ; IsBoundedJoinSemilattice; IsLattice; IsDistributiveLattice
            ; IsBooleanAlgebra)
    open import Level using (suc; _⊔_)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Core using (Rel)

    ------------------------------------------------------------------------
    -- Re-export definitions of 'raw' bundles

    open Raw public
      using (RawLattice)

    ------------------------------------------------------------------------
    -- Bundles
    ------------------------------------------------------------------------

    record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∙_
      infix  4 _≈_
      field
        Carrier       : Set c
        _≈_           : Rel Carrier ℓ
        _∙_           : Op₂ Carrier
        isSemilattice : IsSemilattice _≈_ _∙_

      open IsSemilattice _≈_ isSemilattice public

      band : Band c ℓ
      band = record { isBand = isBand }

      open Band band public
        using (_≉_; rawMagma; magma; isMagma; semigroup; isSemigroup; isBand)

    record MeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∧_
      infix  4 _≈_
      field
        Carrier           : Set c
        _≈_               : Rel Carrier ℓ
        _∧_               : Op₂ Carrier
        isMeetSemilattice : IsSemilattice _≈_ _∧_

      open IsMeetSemilattice _≈_ isMeetSemilattice public

      semilattice : Semilattice c ℓ
      semilattice = record { isSemilattice = isMeetSemilattice }

      open Semilattice semilattice public
        using (rawMagma; magma; semigroup; band)

    record JoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∨_
      infix  4 _≈_
      field
        Carrier           : Set c
        _≈_               : Rel Carrier ℓ
        _∨_               : Op₂ Carrier
        isJoinSemilattice : IsSemilattice _≈_ _∨_

      open IsJoinSemilattice _≈_ isJoinSemilattice public

      semilattice : Semilattice c ℓ
      semilattice = record { isSemilattice = isJoinSemilattice }

      open Semilattice semilattice public
        using (rawMagma; magma; semigroup; band)

    record BoundedSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∙_
      infix  4 _≈_
      field
        Carrier              : Set c
        _≈_                  : Rel Carrier ℓ
        _∙_                  : Op₂ Carrier
        ε                    : Carrier
        isBoundedSemilattice : IsBoundedSemilattice _≈_ _∙_ ε

      open IsBoundedSemilattice _≈_ isBoundedSemilattice public

      semilattice : Semilattice c ℓ
      semilattice = record { isSemilattice = isSemilattice }

      open Semilattice semilattice public using (rawMagma; magma; semigroup; band)

    record BoundedMeetSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∧_
      infix  4 _≈_
      field
        Carrier                  : Set c
        _≈_                      : Rel Carrier ℓ
        _∧_                      : Op₂ Carrier
        ⊤                        : Carrier
        isBoundedMeetSemilattice : IsBoundedSemilattice _≈_ _∧_ ⊤

      open IsBoundedMeetSemilattice _≈_ isBoundedMeetSemilattice public

      boundedSemilattice : BoundedSemilattice c ℓ
      boundedSemilattice = record
        { isBoundedSemilattice = isBoundedMeetSemilattice }

      open BoundedSemilattice boundedSemilattice public
        using (rawMagma; magma; semigroup; band; semilattice)

    record BoundedJoinSemilattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∨_
      infix  4 _≈_
      field
        Carrier                  : Set c
        _≈_                      : Rel Carrier ℓ
        _∨_                      : Op₂ Carrier
        ⊥                        : Carrier
        isBoundedJoinSemilattice : IsBoundedSemilattice _≈_ _∨_ ⊥

      open IsBoundedJoinSemilattice _≈_ isBoundedJoinSemilattice public

      boundedSemilattice : BoundedSemilattice c ℓ
      boundedSemilattice = record
        { isBoundedSemilattice = isBoundedJoinSemilattice }

      open BoundedSemilattice boundedSemilattice public
        using (rawMagma; magma; semigroup; band; semilattice)

    record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∧_
      infixr 6 _∨_
      infix  4 _≈_
      field
        Carrier   : Set c
        _≈_       : Rel Carrier ℓ
        _∨_       : Op₂ Carrier
        _∧_       : Op₂ Carrier
        isLattice : IsLattice _≈_ _∨_ _∧_

      open IsLattice isLattice public

      rawLattice : RawLattice c ℓ
      rawLattice = record
        { _≈_  = _≈_
        ; _∧_  = _∧_
        ; _∨_  = _∨_
        }

      open RawLattice rawLattice public
        using (∨-rawMagma; ∧-rawMagma)

      setoid : Setoid c ℓ
      setoid = record { isEquivalence = isEquivalence }

      open Setoid setoid public
        using (_≉_)

    record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
      infixr 7 _∧_
      infixr 6 _∨_
      infix  4 _≈_
      field
        Carrier               : Set c
        _≈_                   : Rel Carrier ℓ
        _∨_                   : Op₂ Carrier
        _∧_                   : Op₂ Carrier
        isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_

      open IsDistributiveLattice isDistributiveLattice public

      lattice : Lattice _ _
      lattice = record { isLattice = isLattice }

      open Lattice lattice public
        using
        ( _≉_; setoid; rawLattice
        ; ∨-rawMagma; ∧-rawMagma
        )

    record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
      infix  8 ¬_
      infixr 7 _∧_
      infixr 6 _∨_
      infix  4 _≈_
      field
        Carrier          : Set c
        _≈_              : Rel Carrier ℓ
        _∨_              : Op₂ Carrier
        _∧_              : Op₂ Carrier
        ¬_               : Op₁ Carrier
        ⊤                : Carrier
        ⊥                : Carrier
        isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥

      open IsBooleanAlgebra isBooleanAlgebra public

      distributiveLattice : DistributiveLattice _ _
      distributiveLattice = record
        { isDistributiveLattice = isDistributiveLattice
        }

      open DistributiveLattice distributiveLattice public
        using
        ( _≉_; setoid; rawLattice
        ; ∨-rawMagma; ∧-rawMagma
        ; lattice
        )