{-# OPTIONS --cubical-compatible --safe #-}
{-# OPTIONS --warn=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 (_,_)
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."
#-}