    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- This module is DEPRECATED.
    ------------------------------------------------------------------------

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

    -- Disabled to prevent warnings from deprecated names
    {-# OPTIONS --warning=noUserWarning #-}

    open import Algebra.Lattice.Bundles

    module Algebra.Properties.BooleanAlgebra
      {b₁ b₂} (B : BooleanAlgebra b₁ b₂)
      where

    {-# WARNING_ON_IMPORT
    "Algebra.Properties.BooleanAlgebra was deprecated in v2.0.
    Use Algebra.Lattice.Properties.BooleanAlgebra instead."
    #-}

    open import Algebra.Lattice.Properties.BooleanAlgebra B public

    open BooleanAlgebra B

    import Algebra.Properties.DistributiveLattice as DistribLatticeProperties

    open import Algebra.Structures _≈_
    open import Relation.Binary
    open import Function.Bundles using (module Equivalence; _⇔_)
    open import Data.Product.Base using (_,_)

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 1.4

    replace-equality : {_≈′_ : Rel Carrier b₂} →
                       (∀ {x y} → x ≈ y ⇔ (x ≈′ y)) →
                       BooleanAlgebra _ _
    replace-equality {_≈′_} ≈⇔≈′ = record
      { isBooleanAlgebra = record
        { isDistributiveLattice = DistributiveLattice.isDistributiveLattice
            (DistribLatticeProperties.replace-equality distributiveLattice ≈⇔≈′)
        ; ∨-complement          = ((λ x → to (∨-complementˡ x)) , λ x → to (∨-complementʳ x))
        ; ∧-complement          = ((λ x → to (∧-complementˡ x)) , λ x → to (∧-complementʳ x))
        ; ¬-cong                = λ i≈j → to (¬-cong (from i≈j))
        }
      } where open module E {x y} = Equivalence (≈⇔≈′ {x} {y})
    {-# WARNING_ON_USAGE replace-equality
    "Warning: replace-equality was deprecated in v1.4.
    Please use isBooleanAlgebra from `Algebra.Construct.Subst.Equality` instead."
    #-}