{-# OPTIONS --without-K --safe #-}
open import Algebra.Lattice.Bundles
import Algebra.Lattice.Properties.Lattice as LatticeProperties
module Algebra.Lattice.Properties.DistributiveLattice
{dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
where
open DistributiveLattice DL
open import Algebra.Definitions _≈_
open import Algebra.Lattice.Structures _≈_
open import Relation.Binary.Reasoning.Setoid setoid
open LatticeProperties lattice public
∧-∨-isDistributiveLattice : IsDistributiveLattice _∧_ _∨_
∧-∨-isDistributiveLattice = record
{ isLattice = ∧-∨-isLattice
; ∨-distrib-∧ = ∧-distrib-∨
; ∧-distrib-∨ = ∨-distrib-∧
}
∧-∨-distributiveLattice : DistributiveLattice _ _
∧-∨-distributiveLattice = record
{ isDistributiveLattice = ∧-∨-isDistributiveLattice
}