------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of min and max operators specified over a total preorder. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator) open import Relation.Binary.Bundles using (TotalPreorder) module Algebra.Lattice.Construct.NaturalChoice.MinMaxOp {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) (maxOp : MaxOperator O) where open TotalPreorder O open MinOperator minOp open MaxOperator maxOp open import Algebra.Lattice.Structures _≈_ open import Algebra.Construct.NaturalChoice.MinMaxOp minOp maxOp open import Algebra.Lattice.Bundles using (Lattice; DistributiveLattice) open import Relation.Binary.Reasoning.Preorder preorder ------------------------------------------------------------------------ -- Re-export properties of individual operators open import Algebra.Lattice.Construct.NaturalChoice.MinOp minOp public open import Algebra.Lattice.Construct.NaturalChoice.MaxOp maxOp public ------------------------------------------------------------------------ -- Structures ⊔-⊓-isLattice : IsLattice _⊔_ _⊓_ ⊔-⊓-isLattice = record { isEquivalence = isEquivalence ; ∨-comm = ⊔-comm ; ∨-assoc = ⊔-assoc ; ∨-cong = ⊔-cong ; ∧-comm = ⊓-comm ; ∧-assoc = ⊓-assoc ; ∧-cong = ⊓-cong ; absorptive = ⊔-⊓-absorptive } ⊓-⊔-isLattice : IsLattice _⊓_ _⊔_ ⊓-⊔-isLattice = record { isEquivalence = isEquivalence ; ∨-comm = ⊓-comm ; ∨-assoc = ⊓-assoc ; ∨-cong = ⊓-cong ; ∧-comm = ⊔-comm ; ∧-assoc = ⊔-assoc ; ∧-cong = ⊔-cong ; absorptive = ⊓-⊔-absorptive } ⊓-⊔-isDistributiveLattice : IsDistributiveLattice _⊓_ _⊔_ ⊓-⊔-isDistributiveLattice = record { isLattice = ⊓-⊔-isLattice ; ∨-distrib-∧ = ⊓-distrib-⊔ ; ∧-distrib-∨ = ⊔-distrib-⊓ } ⊔-⊓-isDistributiveLattice : IsDistributiveLattice _⊔_ _⊓_ ⊔-⊓-isDistributiveLattice = record { isLattice = ⊔-⊓-isLattice ; ∨-distrib-∧ = ⊔-distrib-⊓ ; ∧-distrib-∨ = ⊓-distrib-⊔ } ------------------------------------------------------------------------ -- Bundles ⊔-⊓-lattice : Lattice _ _ ⊔-⊓-lattice = record { isLattice = ⊔-⊓-isLattice } ⊓-⊔-lattice : Lattice _ _ ⊓-⊔-lattice = record { isLattice = ⊓-⊔-isLattice } ⊔-⊓-distributiveLattice : DistributiveLattice _ _ ⊔-⊓-distributiveLattice = record { isDistributiveLattice = ⊔-⊓-isDistributiveLattice } ⊓-⊔-distributiveLattice : DistributiveLattice _ _ ⊓-⊔-distributiveLattice = record { isDistributiveLattice = ⊓-⊔-isDistributiveLattice }