------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of min and max operators specified over a total preorder.
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Algebra.Lattice.Bundles
open import Algebra.Construct.NaturalChoice.Base
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 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
  }