    ------------------------------------------------------------------------
    -- 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
      }