------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Lattice.Bundles using (DistributiveLattice)

module Algebra.Lattice.Properties.DistributiveLattice
  {dl₁ dl₂} (DL : DistributiveLattice dl₁ dl₂)
  where

import Algebra.Lattice.Properties.Lattice as LatticeProperties
open DistributiveLattice DL
open import Algebra.Definitions _≈_
open import Algebra.Lattice.Structures _≈_
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Export properties of lattices

open LatticeProperties lattice public

------------------------------------------------------------------------
-- The dual construction is also a distributive lattice.

∧-∨-isDistributiveLattice : IsDistributiveLattice _∧_ _∨_
∧-∨-isDistributiveLattice = record
  { isLattice   = ∧-∨-isLattice
  ; ∨-distrib-∧ = ∧-distrib-∨
  ; ∧-distrib-∨ = ∨-distrib-∧
  }

∧-∨-distributiveLattice : DistributiveLattice _ _
∧-∨-distributiveLattice = record
  { isDistributiveLattice = ∧-∨-isDistributiveLattice
  }