------------------------------------------------------------------------ -- 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 using (Op₁; Op₂) 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 4 _≈_ _≤_ infixr 6 _∨_ 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 4 _≈_ _≤_ infixr 6 _∨_ 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 4 _≈_ _≤_ infixr 7 _∧_ 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 4 _≈_ _≤_ infixr 7 _∧_ 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 4 _≈_ _≤_ infixr 6 _∨_ infixr 7 _∧_ 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 4 _≈_ _≤_ infixr 6 _∨_ infixr 7 _∧_ 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 4 _≈_ _≤_ infixr 6 _∨_ infixr 7 _∧_ 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 4 _≈_ _≤_ infixr 5 _⇨_ infixr 6 _∨_ infixr 7 _∧_ 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 4 _≈_ _≤_ infixr 6 _∨_ infixr 7 _∧_ infix 8 ¬_ 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; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥)