```------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties of Boolean algebras
------------------------------------------------------------------------

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

open import Algebra.Lattice.Bundles

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

open BooleanAlgebra B

import Algebra.Lattice.Properties.DistributiveLattice as DistribLatticeProperties
open import Algebra.Core
open import Algebra.Structures _≈_
open import Algebra.Definitions _≈_
open import Algebra.Consequences.Setoid setoid
open import Algebra.Bundles
open import Algebra.Lattice.Structures _≈_
open import Relation.Binary.Reasoning.Setoid setoid
open import Relation.Binary
open import Function.Base
open import Function.Bundles using (_⇔_; module Equivalence)
open import Data.Product using (_,_)

------------------------------------------------------------------------
-- Export properties from distributive lattices

open DistribLatticeProperties distributiveLattice public

------------------------------------------------------------------------
-- The dual construction is also a boolean algebra

∧-∨-isBooleanAlgebra : IsBooleanAlgebra _∧_ _∨_ ¬_ ⊥ ⊤
∧-∨-isBooleanAlgebra = record
{ isDistributiveLattice = ∧-∨-isDistributiveLattice
; ∨-complement          = ∧-complement
; ∧-complement          = ∨-complement
; ¬-cong                = ¬-cong
}

∧-∨-booleanAlgebra : BooleanAlgebra _ _
∧-∨-booleanAlgebra = record
{ isBooleanAlgebra = ∧-∨-isBooleanAlgebra
}

------------------------------------------------------------------------
-- (∨, ∧, ⊥, ⊤) and (∧, ∨, ⊤, ⊥) are commutative semirings

∧-identityʳ : RightIdentity ⊤ _∧_
∧-identityʳ x = begin
x ∧ ⊤          ≈⟨ ∧-congˡ (sym (∨-complementʳ _)) ⟩
x ∧ (x ∨ ¬ x)  ≈⟨ ∧-absorbs-∨ _ _ ⟩
x              ∎

∧-identityˡ : LeftIdentity ⊤ _∧_
∧-identityˡ = comm+idʳ⇒idˡ ∧-comm ∧-identityʳ

∧-identity : Identity ⊤ _∧_
∧-identity = ∧-identityˡ , ∧-identityʳ

∨-identityʳ : RightIdentity ⊥ _∨_
∨-identityʳ x = begin
x ∨ ⊥          ≈⟨ ∨-congˡ \$ sym (∧-complementʳ _) ⟩
x ∨ x ∧ ¬ x    ≈⟨ ∨-absorbs-∧ _ _ ⟩
x              ∎

∨-identityˡ : LeftIdentity ⊥ _∨_
∨-identityˡ = comm+idʳ⇒idˡ ∨-comm ∨-identityʳ

∨-identity : Identity ⊥ _∨_
∨-identity = ∨-identityˡ , ∨-identityʳ

∧-zeroʳ : RightZero ⊥ _∧_
∧-zeroʳ x = begin
x ∧ ⊥          ≈˘⟨ ∧-congˡ (∧-complementʳ x) ⟩
x ∧  x  ∧ ¬ x  ≈˘⟨ ∧-assoc x x (¬ x) ⟩
(x ∧ x) ∧ ¬ x  ≈⟨  ∧-congʳ (∧-idem x) ⟩
x       ∧ ¬ x  ≈⟨  ∧-complementʳ x ⟩
⊥              ∎

∧-zeroˡ : LeftZero ⊥ _∧_
∧-zeroˡ = comm+zeʳ⇒zeˡ ∧-comm ∧-zeroʳ

∧-zero : Zero ⊥ _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ

∨-zeroʳ : ∀ x → x ∨ ⊤ ≈ ⊤
∨-zeroʳ x = begin
x ∨ ⊤          ≈˘⟨ ∨-congˡ (∨-complementʳ x) ⟩
x ∨  x  ∨ ¬ x  ≈˘⟨ ∨-assoc x x (¬ x) ⟩
(x ∨ x) ∨ ¬ x  ≈⟨ ∨-congʳ (∨-idem x) ⟩
x       ∨ ¬ x  ≈⟨ ∨-complementʳ x ⟩
⊤              ∎

∨-zeroˡ : LeftZero ⊤ _∨_
∨-zeroˡ = comm+zeʳ⇒zeˡ ∨-comm ∨-zeroʳ

∨-zero : Zero ⊤ _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ

∨-⊥-isMonoid : IsMonoid _∨_ ⊥
∨-⊥-isMonoid = record
{ isSemigroup = ∨-isSemigroup
; identity    = ∨-identity
}

∧-⊤-isMonoid : IsMonoid _∧_ ⊤
∧-⊤-isMonoid = record
{ isSemigroup = ∧-isSemigroup
; identity    = ∧-identity
}

∨-⊥-isCommutativeMonoid : IsCommutativeMonoid _∨_ ⊥
∨-⊥-isCommutativeMonoid = record
{ isMonoid = ∨-⊥-isMonoid
; comm     = ∨-comm
}

∧-⊤-isCommutativeMonoid : IsCommutativeMonoid _∧_ ⊤
∧-⊤-isCommutativeMonoid = record
{ isMonoid = ∧-⊤-isMonoid
; comm     = ∧-comm
}

∨-∧-isSemiring : IsSemiring _∨_ _∧_ ⊥ ⊤
∨-∧-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∨-⊥-isCommutativeMonoid
; *-cong = ∧-cong
; *-assoc = ∧-assoc
; *-identity = ∧-identity
; distrib = ∧-distrib-∨
}
; zero = ∧-zero
}

∧-∨-isSemiring : IsSemiring _∧_ _∨_ ⊤ ⊥
∧-∨-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∧-⊤-isCommutativeMonoid
; *-cong = ∨-cong
; *-assoc = ∨-assoc
; *-identity = ∨-identity
; distrib = ∨-distrib-∧
}
; zero = ∨-zero
}

∨-∧-isCommutativeSemiring : IsCommutativeSemiring _∨_ _∧_ ⊥ ⊤
∨-∧-isCommutativeSemiring = record
{ isSemiring = ∨-∧-isSemiring
; *-comm = ∧-comm
}

∧-∨-isCommutativeSemiring : IsCommutativeSemiring _∧_ _∨_ ⊤ ⊥
∧-∨-isCommutativeSemiring = record
{ isSemiring = ∧-∨-isSemiring
; *-comm = ∨-comm
}

∨-∧-commutativeSemiring : CommutativeSemiring _ _
∨-∧-commutativeSemiring = record
{ isCommutativeSemiring = ∨-∧-isCommutativeSemiring
}

∧-∨-commutativeSemiring : CommutativeSemiring _ _
∧-∨-commutativeSemiring = record
{ isCommutativeSemiring = ∧-∨-isCommutativeSemiring
}

------------------------------------------------------------------------
-- Some other properties

-- I took the statement of this lemma (called Uniqueness of
-- Complements) from some course notes, "Boolean Algebra", written
-- by Gert Smolka.

private
lemma : ∀ x y → x ∧ y ≈ ⊥ → x ∨ y ≈ ⊤ → ¬ x ≈ y
lemma x y x∧y=⊥ x∨y=⊤ = begin
¬ x                ≈˘⟨ ∧-identityʳ _ ⟩
¬ x ∧ ⊤            ≈˘⟨ ∧-congˡ x∨y=⊤ ⟩
¬ x ∧ (x ∨ y)      ≈⟨  ∧-distribˡ-∨ _ _ _ ⟩
¬ x ∧ x ∨ ¬ x ∧ y  ≈⟨  ∨-congʳ \$ ∧-complementˡ _ ⟩
⊥ ∨ ¬ x ∧ y        ≈˘⟨ ∨-congʳ x∧y=⊥ ⟩
x ∧ y ∨ ¬ x ∧ y    ≈˘⟨ ∧-distribʳ-∨ _ _ _ ⟩
(x ∨ ¬ x) ∧ y      ≈⟨  ∧-congʳ \$ ∨-complementʳ _ ⟩
⊤ ∧ y              ≈⟨  ∧-identityˡ _ ⟩
y                  ∎

⊥≉⊤ : ¬ ⊥ ≈ ⊤
⊥≉⊤ = lemma ⊥ ⊤ (∧-identityʳ _) (∨-zeroʳ _)

⊤≉⊥ : ¬ ⊤ ≈ ⊥
⊤≉⊥ = lemma ⊤ ⊥ (∧-zeroʳ _) (∨-identityʳ _)

¬-involutive : Involutive ¬_
¬-involutive x = lemma (¬ x) x (∧-complementˡ _) (∨-complementˡ _)

deMorgan₁ : ∀ x y → ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y
deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂
where
lem₁ = begin
(x ∧ y) ∧ (¬ x ∨ ¬ y)          ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩
(x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∨-congʳ \$ ∧-congʳ \$ ∧-comm _ _ ⟩
(y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y  ≈⟨ ∧-assoc _ _ _ ⟨ ∨-cong ⟩ ∧-assoc _ _ _ ⟩
y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y)  ≈⟨ (∧-congˡ \$ ∧-complementʳ _) ⟨ ∨-cong ⟩
(∧-congˡ \$ ∧-complementʳ _) ⟩
(y ∧ ⊥) ∨ (x ∧ ⊥)              ≈⟨ ∧-zeroʳ _ ⟨ ∨-cong ⟩ ∧-zeroʳ _ ⟩
⊥ ∨ ⊥                          ≈⟨ ∨-identityʳ _ ⟩
⊥                              ∎

lem₃ = begin
(x ∧ y) ∨ ¬ x          ≈⟨ ∨-distribʳ-∧ _ _ _ ⟩
(x ∨ ¬ x) ∧ (y ∨ ¬ x)  ≈⟨ ∧-congʳ \$ ∨-complementʳ _ ⟩
⊤ ∧ (y ∨ ¬ x)          ≈⟨ ∧-identityˡ _ ⟩
y ∨ ¬ x                ≈⟨ ∨-comm _ _ ⟩
¬ x ∨ y                ∎

lem₂ = begin
(x ∧ y) ∨ (¬ x ∨ ¬ y)  ≈˘⟨ ∨-assoc _ _ _ ⟩
((x ∧ y) ∨ ¬ x) ∨ ¬ y  ≈⟨ ∨-congʳ lem₃ ⟩
(¬ x ∨ y) ∨ ¬ y        ≈⟨ ∨-assoc _ _ _ ⟩
¬ x ∨ (y ∨ ¬ y)        ≈⟨ ∨-congˡ \$ ∨-complementʳ _ ⟩
¬ x ∨ ⊤                ≈⟨ ∨-zeroʳ _ ⟩
⊤                      ∎

deMorgan₂ : ∀ x y → ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y
deMorgan₂ x y = begin
¬ (x ∨ y)          ≈˘⟨ ¬-cong \$ ((¬-involutive _) ⟨ ∨-cong ⟩ (¬-involutive _)) ⟩
¬ (¬ ¬ x ∨ ¬ ¬ y)  ≈˘⟨ ¬-cong \$ deMorgan₁ _ _ ⟩
¬ ¬ (¬ x ∧ ¬ y)    ≈⟨ ¬-involutive _ ⟩
¬ x ∧ ¬ y          ∎

------------------------------------------------------------------------
-- (⊕, ∧, id, ⊥, ⊤) is a commutative ring

-- This construction is parameterised over the definition of xor.

module XorRing
(xor : Op₂ Carrier)
(⊕-def : ∀ x y → xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y))
where

private
infixl 6 _⊕_

_⊕_ : Op₂ Carrier
_⊕_ = xor

helper : ∀ {x y u v} → x ≈ y → u ≈ v → x ∧ ¬ u ≈ y ∧ ¬ v
helper x≈y u≈v = x≈y ⟨ ∧-cong ⟩ ¬-cong u≈v

⊕-cong : Congruent₂ _⊕_
⊕-cong {x} {y} {u} {v} x≈y u≈v = begin
x ⊕ u                ≈⟨  ⊕-def _ _ ⟩
(x ∨ u) ∧ ¬ (x ∧ u)  ≈⟨  helper (x≈y ⟨ ∨-cong ⟩ u≈v)
(x≈y ⟨ ∧-cong ⟩ u≈v) ⟩
(y ∨ v) ∧ ¬ (y ∧ v)  ≈˘⟨ ⊕-def _ _ ⟩
y ⊕ v                ∎

⊕-comm : Commutative _⊕_
⊕-comm x y = begin
x ⊕ y                ≈⟨  ⊕-def _ _ ⟩
(x ∨ y) ∧ ¬ (x ∧ y)  ≈⟨  helper (∨-comm _ _) (∧-comm _ _) ⟩
(y ∨ x) ∧ ¬ (y ∧ x)  ≈˘⟨ ⊕-def _ _ ⟩
y ⊕ x                ∎

¬-distribˡ-⊕ : ∀ x y → ¬ (x ⊕ y) ≈ ¬ x ⊕ y
¬-distribˡ-⊕ x y = begin
¬ (x ⊕ y)                              ≈⟨ ¬-cong \$ ⊕-def _ _ ⟩
¬ ((x ∨ y) ∧ (¬ (x ∧ y)))              ≈⟨ ¬-cong (∧-distribʳ-∨ _ _ _) ⟩
¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y)))  ≈⟨ ¬-cong \$ ∨-congˡ \$ ∧-congˡ \$ ¬-cong (∧-comm _ _) ⟩
¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x)))  ≈⟨ ¬-cong \$ lem _ _ ⟨ ∨-cong ⟩ lem _ _ ⟩
¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x))              ≈⟨ deMorgan₂ _ _ ⟩
¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x)              ≈⟨ ∧-congʳ \$ deMorgan₁ _ _ ⟩
(¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x)          ≈⟨ helper (∨-congˡ \$ ¬-involutive _) (∧-comm _ _) ⟩
(¬ x ∨ y) ∧ ¬ (¬ x ∧ y)                ≈˘⟨ ⊕-def _ _ ⟩
¬ x ⊕ y                                ∎
where
lem : ∀ x y → x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y
lem x y = begin
x ∧ ¬ (x ∧ y)          ≈⟨ ∧-congˡ \$ deMorgan₁ _ _ ⟩
x ∧ (¬ x ∨ ¬ y)        ≈⟨ ∧-distribˡ-∨ _ _ _ ⟩
(x ∧ ¬ x) ∨ (x ∧ ¬ y)  ≈⟨ ∨-congʳ \$ ∧-complementʳ _ ⟩
⊥ ∨ (x ∧ ¬ y)          ≈⟨ ∨-identityˡ _ ⟩
x ∧ ¬ y                ∎

¬-distribʳ-⊕ : ∀ x y → ¬ (x ⊕ y) ≈ x ⊕ ¬ y
¬-distribʳ-⊕ x y = begin
¬ (x ⊕ y)  ≈⟨ ¬-cong \$ ⊕-comm _ _ ⟩
¬ (y ⊕ x)  ≈⟨ ¬-distribˡ-⊕ _ _ ⟩
¬ y ⊕ x    ≈⟨ ⊕-comm _ _ ⟩
x ⊕ ¬ y    ∎

⊕-annihilates-¬ : ∀ x y → x ⊕ y ≈ ¬ x ⊕ ¬ y
⊕-annihilates-¬ x y = begin
x ⊕ y        ≈˘⟨ ¬-involutive _ ⟩
¬ ¬ (x ⊕ y)  ≈⟨  ¬-cong \$ ¬-distribˡ-⊕ _ _ ⟩
¬ (¬ x ⊕ y)  ≈⟨  ¬-distribʳ-⊕ _ _ ⟩
¬ x ⊕ ¬ y    ∎

⊕-identityˡ : LeftIdentity ⊥ _⊕_
⊕-identityˡ x = begin
⊥ ⊕ x                ≈⟨ ⊕-def _ _ ⟩
(⊥ ∨ x) ∧ ¬ (⊥ ∧ x)  ≈⟨ helper (∨-identityˡ _) (∧-zeroˡ _) ⟩
x ∧ ¬ ⊥              ≈⟨ ∧-congˡ ⊥≉⊤ ⟩
x ∧ ⊤                ≈⟨ ∧-identityʳ _ ⟩
x                    ∎

⊕-identityʳ : RightIdentity ⊥ _⊕_
⊕-identityʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-identityˡ _

⊕-identity : Identity ⊥ _⊕_
⊕-identity = ⊕-identityˡ , ⊕-identityʳ

⊕-inverseˡ : LeftInverse ⊥ id _⊕_
⊕-inverseˡ x = begin
x ⊕ x               ≈⟨ ⊕-def _ _ ⟩
(x ∨ x) ∧ ¬ (x ∧ x) ≈⟨ helper (∨-idem _) (∧-idem _) ⟩
x ∧ ¬ x             ≈⟨ ∧-complementʳ _ ⟩
⊥                   ∎

⊕-inverseʳ : RightInverse ⊥ id _⊕_
⊕-inverseʳ _ = ⊕-comm _ _ ⟨ trans ⟩ ⊕-inverseˡ _

⊕-inverse : Inverse ⊥ id _⊕_
⊕-inverse = ⊕-inverseˡ , ⊕-inverseʳ

∧-distribˡ-⊕ : _∧_ DistributesOverˡ _⊕_
∧-distribˡ-⊕ x y z = begin
x ∧ (y ⊕ z)                ≈⟨ ∧-congˡ \$ ⊕-def _ _ ⟩
x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈˘⟨ ∧-assoc _ _ _ ⟩
(x ∧ (y ∨ z)) ∧ ¬ (y ∧ z)  ≈⟨ ∧-congˡ \$ deMorgan₁ _ _ ⟩
(x ∧ (y ∨ z)) ∧
(¬ y ∨ ¬ z)                ≈˘⟨ ∨-identityˡ _ ⟩
⊥ ∨
((x ∧ (y ∨ z)) ∧
(¬ y ∨ ¬ z))               ≈⟨ ∨-congʳ lem₃ ⟩
((x ∧ (y ∨ z)) ∧ ¬ x) ∨
((x ∧ (y ∨ z)) ∧
(¬ y ∨ ¬ z))               ≈˘⟨ ∧-distribˡ-∨ _ _ _ ⟩
(x ∧ (y ∨ z)) ∧
(¬ x ∨ (¬ y ∨ ¬ z))        ≈˘⟨ ∧-congˡ \$ ∨-congˡ (deMorgan₁ _ _) ⟩
(x ∧ (y ∨ z)) ∧
(¬ x ∨ ¬ (y ∧ z))          ≈˘⟨ ∧-congˡ (deMorgan₁ _ _) ⟩
(x ∧ (y ∨ z)) ∧
¬ (x ∧ (y ∧ z))            ≈⟨ helper refl lem₁ ⟩
(x ∧ (y ∨ z)) ∧
¬ ((x ∧ y) ∧ (x ∧ z))      ≈⟨ ∧-congʳ \$ ∧-distribˡ-∨ _ _ _ ⟩
((x ∧ y) ∨ (x ∧ z)) ∧
¬ ((x ∧ y) ∧ (x ∧ z))      ≈˘⟨ ⊕-def _ _ ⟩
(x ∧ y) ⊕ (x ∧ z)          ∎
where
lem₂ = begin
x ∧ (y ∧ z)  ≈˘⟨ ∧-assoc _ _ _ ⟩
(x ∧ y) ∧ z  ≈⟨ ∧-congʳ \$ ∧-comm _ _ ⟩
(y ∧ x) ∧ z  ≈⟨ ∧-assoc _ _ _ ⟩
y ∧ (x ∧ z)  ∎

lem₁ = begin
x ∧ (y ∧ z)        ≈˘⟨ ∧-congʳ (∧-idem _) ⟩
(x ∧ x) ∧ (y ∧ z)  ≈⟨ ∧-assoc _ _ _ ⟩
x ∧ (x ∧ (y ∧ z))  ≈⟨ ∧-congˡ lem₂ ⟩
x ∧ (y ∧ (x ∧ z))  ≈˘⟨ ∧-assoc _ _ _ ⟩
(x ∧ y) ∧ (x ∧ z)  ∎

lem₃ = begin
⊥                      ≈˘⟨ ∧-zeroʳ _ ⟩
(y ∨ z) ∧ ⊥            ≈˘⟨ ∧-congˡ (∧-complementʳ _) ⟩
(y ∨ z) ∧ (x ∧ ¬ x)    ≈˘⟨ ∧-assoc _ _ _ ⟩
((y ∨ z) ∧ x) ∧ ¬ x    ≈⟨ ∧-comm _ _ ⟨ ∧-cong ⟩ refl  ⟩
(x ∧ (y ∨ z)) ∧ ¬ x    ∎

∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_
∧-distribʳ-⊕ = comm+distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕

∧-distrib-⊕ : _∧_ DistributesOver _⊕_
∧-distrib-⊕ = ∧-distribˡ-⊕ , ∧-distribʳ-⊕

private

lemma₂ : ∀ x y u v →
(x ∧ y) ∨ (u ∧ v) ≈
((x ∨ u) ∧ (y ∨ u)) ∧
((x ∨ v) ∧ (y ∨ v))
lemma₂ x y u v = begin
(x ∧ y) ∨ (u ∧ v)              ≈⟨ ∨-distribˡ-∧ _ _ _ ⟩
((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v)  ≈⟨ ∨-distribʳ-∧ _ _ _
⟨ ∧-cong ⟩
∨-distribʳ-∧ _ _ _ ⟩
((x ∨ u) ∧ (y ∨ u)) ∧
((x ∨ v) ∧ (y ∨ v))            ∎

⊕-assoc : Associative _⊕_
⊕-assoc x y z = sym \$ begin
x ⊕ (y ⊕ z)                                ≈⟨ refl ⟨ ⊕-cong ⟩ ⊕-def _ _ ⟩
x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z))                  ≈⟨ ⊕-def _ _ ⟩
(x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))) ∧
¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))              ≈⟨ lem₃ ⟨ ∧-cong ⟩ lem₄ ⟩
(((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ ∧-assoc _ _ _ ⟩
((x ∨ y) ∨ z) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈⟨ ∧-congˡ lem₅ ⟩
((x ∨ y) ∨ z) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)))  ≈˘⟨ ∧-assoc _ _ _ ⟩
(((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈⟨ lem₁ ⟨ ∧-cong ⟩ lem₂ ⟩
(((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z) ∧
¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)              ≈˘⟨ ⊕-def _ _ ⟩
((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z                  ≈˘⟨ ⊕-def _ _ ⟨ ⊕-cong ⟩ refl ⟩
(x ⊕ y) ⊕ z                                ∎
where
lem₁ = begin
((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)  ≈˘⟨ ∨-distribʳ-∧ _ _ _ ⟩
((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z        ≈˘⟨ ∨-congʳ \$ ∧-congˡ (deMorgan₁ _ _) ⟩
((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z          ∎

lem₂′ = begin
(x ∨ ¬ y) ∧ (¬ x ∨ y)              ≈˘⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
(⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤)  ≈˘⟨  (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
⟨ ∧-cong ⟩
(∧-congˡ \$ ∨-complementˡ _) ⟩
((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧
((¬ x ∨ y) ∧ (¬ y ∨ y))            ≈˘⟨ lemma₂ _ _ _ _ ⟩
(¬ x ∧ ¬ y) ∨ (x ∧ y)              ≈˘⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y)            ≈˘⟨ deMorgan₁ _ _ ⟩
¬ ((x ∨ y) ∧ ¬ (x ∧ y))            ∎

lem₂ = begin
((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)  ≈˘⟨ ∨-distribʳ-∧ _ _ _ ⟩
((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z          ≈⟨ ∨-congʳ lem₂′ ⟩
¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z          ≈˘⟨ deMorgan₁ _ _ ⟩
¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z)          ∎

lem₃ = begin
x ∨ ((y ∨ z) ∧ ¬ (y ∧ z))          ≈⟨ ∨-congˡ \$ ∧-congˡ \$ deMorgan₁ _ _ ⟩
x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z))        ≈⟨ ∨-distribˡ-∧ _ _ _ ⟩
(x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z))  ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)  ∎

lem₄′ = begin
¬ ((y ∨ z) ∧ ¬ (y ∧ z))    ≈⟨ deMorgan₁ _ _ ⟩
¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z)    ≈⟨ deMorgan₂ _ _ ⟨ ∨-cong ⟩ ¬-involutive _ ⟩
(¬ y ∧ ¬ z) ∨ (y ∧ z)      ≈⟨ lemma₂ _ _ _ _ ⟩
((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧
((¬ y ∨ z) ∧ (¬ z ∨ z))    ≈⟨ (∨-complementˡ _ ⟨ ∧-cong ⟩ ∨-comm _ _)
⟨ ∧-cong ⟩
(∧-congˡ \$ ∨-complementˡ _) ⟩
(⊤ ∧ (y ∨ ¬ z)) ∧
((¬ y ∨ z) ∧ ⊤)            ≈⟨ ∧-identityˡ _ ⟨ ∧-cong ⟩ ∧-identityʳ _ ⟩
(y ∨ ¬ z) ∧ (¬ y ∨ z)      ∎

lem₄ = begin
¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)))  ≈⟨ deMorgan₁ _ _ ⟩
¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z))  ≈⟨ ∨-congˡ lem₄′ ⟩
¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z))  ≈⟨ ∨-distribˡ-∧ _ _ _ ⟩
(¬ x ∨ (y     ∨ ¬ z)) ∧
(¬ x ∨ (¬ y ∨ z))              ≈˘⟨ ∨-assoc _ _ _ ⟨ ∧-cong ⟩ ∨-assoc _ _ _ ⟩
((¬ x ∨ y)     ∨ ¬ z) ∧
((¬ x ∨ ¬ y) ∨ z)              ≈⟨ ∧-comm _ _ ⟩
((¬ x ∨ ¬ y) ∨ z) ∧
((¬ x ∨ y)     ∨ ¬ z)          ∎

lem₅ = begin
((x ∨ ¬ y) ∨ ¬ z) ∧
(((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ≈˘⟨ ∧-assoc _ _ _ ⟩
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧
((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-congʳ \$ ∧-comm _ _ ⟩
(((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧
((¬ x ∨ y) ∨ ¬ z)                          ≈⟨ ∧-assoc _ _ _ ⟩
((¬ x ∨ ¬ y) ∨ z) ∧
(((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))    ∎

⊕-isMagma : IsMagma _⊕_
⊕-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong        = ⊕-cong
}

⊕-isSemigroup : IsSemigroup _⊕_
⊕-isSemigroup = record
{ isMagma = ⊕-isMagma
; assoc   = ⊕-assoc
}

⊕-⊥-isMonoid : IsMonoid _⊕_ ⊥
⊕-⊥-isMonoid = record
{ isSemigroup = ⊕-isSemigroup
; identity    = ⊕-identity
}

⊕-⊥-isGroup : IsGroup _⊕_ ⊥ id
⊕-⊥-isGroup = record
{ isMonoid = ⊕-⊥-isMonoid
; inverse  = ⊕-inverse
; ⁻¹-cong  = id
}

⊕-⊥-isAbelianGroup : IsAbelianGroup _⊕_ ⊥ id
⊕-⊥-isAbelianGroup = record
{ isGroup = ⊕-⊥-isGroup
; comm    = ⊕-comm
}

⊕-∧-isRing : IsRing _⊕_ _∧_ id ⊥ ⊤
⊕-∧-isRing = record
{ +-isAbelianGroup = ⊕-⊥-isAbelianGroup
; *-cong = ∧-cong
; *-assoc = ∧-assoc
; *-identity = ∧-identity
; distrib = ∧-distrib-⊕
; zero = ∧-zero
}

⊕-∧-isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤
⊕-∧-isCommutativeRing = record
{ isRing = ⊕-∧-isRing
; *-comm = ∧-comm
}

⊕-∧-commutativeRing : CommutativeRing _ _
⊕-∧-commutativeRing = record
{ isCommutativeRing = ⊕-∧-isCommutativeRing
}

infixl 6 _⊕_

_⊕_ : Op₂ Carrier
x ⊕ y = (x ∨ y) ∧ ¬ (x ∧ y)

module DefaultXorRing = XorRing _⊕_ (λ _ _ → refl)
```