But we're talking about xor for the Word64 type, so it is slightly more complicated to prove that it has a unit.

Here's a proof in Agda: -- Agda proof that zero is the unit (i.e. - left and right identity) -- for the XOR operation. import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _^_) -- Binary data. data Bin : Set where ⟨⟩ : Bin _O : Bin → Bin _I : Bin → Bin _xor_ : Bin → Bin → Bin ⟨⟩ xor y = y (x O) xor ⟨⟩ = x O (x O) xor (y O) = (x xor y) O (x O) xor (y I) = (x xor y) I (x I) xor ⟨⟩ = x I (x I) xor (y O) = (x xor y) I (x I) xor (y I) = (x xor y) O lemma : ∀ (b : Bin) ------------ → b xor ⟨⟩ ≡ b lemma ⟨⟩ = refl lemma (b O) = refl lemma (b I) = refl _ : ( ⟨⟩ I O O I O I I O ) xor ( ⟨⟩ O I I I O O O O ) ---------------------- ≡ ( ⟨⟩ I I I O O I I O ) _ = refl -- Left & right identity proofs. postulate binO : (⟨⟩ O) ≡ ⟨⟩ -- Just accomodating a syntactical nuisance. xor-idₗ : ∀ (b : Bin) ---------------- → (⟨⟩ O) xor b ≡ b xor-idₗ ⟨⟩ rewrite binO = refl xor-idₗ (b O) = refl xor-idₗ (b I) = refl xor-idᵣ : ∀ (b : Bin) ---------------- → b xor (⟨⟩ O) ≡ b xor-idᵣ ⟨⟩ rewrite binO = refl xor-idᵣ (b O) rewrite lemma b = refl xor-idᵣ (b I) rewrite lemma b = refl -db