{-# OPTIONS --without-K --safe #-}
module Relation.Binary.Lattice.Bundles where
open import Algebra.Core
open import Level using (suc; _⊔_)
open import Relation.Binary
open import Relation.Binary.Lattice.Structures
record JoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
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 ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
⊥ : Carrier
isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥
open IsBoundedJoinSemilattice isBoundedJoinSemilattice public
joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }
open JoinSemilattice joinSemilattice public using (preorder; poset)
record MeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∧_ : Op₂ Carrier
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 ℓ₁
_≤_ : Rel Carrier ℓ₂
_∧_ : Op₂ Carrier
⊤ : Carrier
isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤
open IsBoundedMeetSemilattice isBoundedMeetSemilattice public
meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }
open MeetSemilattice meetSemilattice public using (preorder; poset)
record Lattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
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 ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
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 ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
⊤ : Carrier
⊥ : Carrier
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)
record HeytingAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 5 _⇨_
infixr 6 _∨_
infixr 7 _∧_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
_⇨_ : Op₂ Carrier
⊤ : Carrier
⊥ : Carrier
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
record BooleanAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
infixr 6 _∨_
infixr 7 _∧_
infix 8 ¬_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
_∨_ : Op₂ Carrier
_∧_ : Op₂ Carrier
¬_ : Op₁ Carrier
⊤ : Carrier
⊥ : Carrier
isBooleanAlgebra : IsBooleanAlgebra _≈_ _≤_ _∨_ _∧_ ¬_ ⊤ ⊥
open IsBooleanAlgebra isBooleanAlgebra using (isHeytingAlgebra)
heytingAlgebra : HeytingAlgebra c ℓ₁ ℓ₂
heytingAlgebra = record { isHeytingAlgebra = isHeytingAlgebra }
open HeytingAlgebra heytingAlgebra public
hiding (Carrier; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥)