Homoporphisms.agda

module plfa.part1.Homomorphisms where


import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym; trans; subst; _≢_; subst₂ )
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Nat
open import Data.Nat.Properties

-- open import Function using (_∘_)

open import Data.Product using (_×_; proj₁; proj₂; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Nullary using (¬_)
import Relation.Nullary.Negation using (contraposition)

open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)

open import plfa.part1.Lemmas

data Bit : Set where
  Z : Bit
  I : Bit

data Dec-Bit (b : Bit) : Set where
  Z : b ≡ Z → Dec-Bit b
  I : b ≡ I → Dec-Bit b

decideBit : (b : Bit) → Dec-Bit b
decideBit Z = Z refl
decideBit I = I refl

⨆ : Bit → Bit → Bit
⨆ a Z = a
⨆ Z b = b
⨆ I _ = I

⨅ : Bit → Bit → Bit
⨅ _ Z = Z
⨅ Z _ = Z
⨅ I I = I

⨅-comm : (a b : Bit) → ⨅ a b ≡ ⨅ b a
⨅-comm Z Z = refl
⨅-comm Z I = refl
⨅-comm I Z = refl
⨅-comm I I = refl

⨅-Zʳ : (a : Bit) → ⨅ a Z ≡ Z
⨅-Zʳ Z = refl
⨅-Zʳ I = refl

⨅-Zˡ : (b : Bit) → ⨅ Z b ≡ Z
⨅-Zˡ Z = refl
⨅-Zˡ I = refl

⨅-Iʳ : (a : Bit) → ⨅ a I ≡ a
⨅-Iʳ Z = refl
⨅-Iʳ I = refl

⨅-Iˡ : (b : Bit) → ⨅ I b ≡ b
⨅-Iˡ Z = refl
⨅-Iˡ I = refl

⨆-refl : {a : Bit} → ⨆ a a ≡ a
⨆-refl {Z} = refl
⨆-refl {I} = refl

⨆-Zˡ : ∀ b → ⨆ Z b ≡ b
⨆-Zˡ Z = refl
⨆-Zˡ I = refl

⨆-Zʳ : ∀ a → ⨆ a Z ≡ a
⨆-Zʳ Z = refl
⨆-Zʳ I = refl

⨆-Z : {a b : Bit} → ⨆ a b ≡ Z → a ≡ Z × b ≡ Z
⨆-Z {Z} {I} ()
⨆-Z {I} {Z} ()
⨆-Z {Z} {Z} abz = refl , refl

⨆-Iˡ : ∀ b → ⨆ I b ≡ I
⨆-Iˡ Z = refl
⨆-Iˡ I = refl

⨆-Iʳ : ∀ a → ⨆ a I ≡ I
⨆-Iʳ Z = refl
⨆-Iʳ I = refl

⨆-assoc : (a b c : Bit) → ⨆ a (⨆ b c) ≡ ⨆ (⨆ a b) c
⨆-assoc Z b c rewrite ⨆-Zˡ (⨆ b c) | ⨆-Zˡ b = refl
⨆-assoc I b c rewrite ⨆-Iˡ (⨆ b c) | ⨆-Iˡ b | ⨆-Iˡ c = refl

⨆-comm : (a b : Bit) → ⨆ a b ≡ ⨆ b a
⨆-comm Z b = begin
  ⨆ Z b  ≡⟨ ⨆-Zˡ b ⟩
  b      ≡⟨ sym $ ⨆-Zʳ b ⟩
  ⨆ b Z  ∎
⨆-comm I b = begin
  ⨆ I b  ≡⟨ ⨆-Iˡ b ⟩
  I      ≡⟨ sym $ ⨆-Iʳ b ⟩
  ⨆ b I  ∎

⨆-comm² : (a b c : Bit) → ⨆ a (⨆ b c) ≡ ⨆ b (⨆ a c)
⨆-comm² a b c = begin
  ⨆ a (⨆ b c)  ≡⟨ ⨆-assoc a b c ⟩
  ⨆ (⨆ a b) c  ≡⟨ cong (λ x → ⨆ x c) $ ⨆-comm a b ⟩
  ⨆ (⨆ b a) c  ≡⟨ sym $ ⨆-assoc b a c ⟩
  ⨆ b (⨆ a c)  ∎

!ᵇ_ : Bit → Bit
!ᵇ Z = I
!ᵇ I = Z

_⊕_ : Bit → Bit → Bit
_⊕_ Z b = b
_⊕_ a Z = a
_⊕_ I I = Z

infixr 6 _⊕_

⊕-identityʳ : (a : Bit) → a ⊕ Z ≡ a
⊕-identityʳ Z = refl
⊕-identityʳ I = refl

⊕-identityˡ : (a : Bit) → Z ⊕ a ≡ a
⊕-identityˡ Z = refl
⊕-identityˡ I = refl

⊕-elim : (a : Bit) → a ⊕ a ≡ Z
⊕-elim Z = refl
⊕-elim I = refl

⊕-II : (a : Bit) → I ⊕ I ⊕ a ≡ a
⊕-II Z = refl
⊕-II I = refl

⊕-assoc : (a b c : Bit) → a ⊕ (b ⊕ c) ≡ (a ⊕ b) ⊕ c
⊕-assoc a Z c rewrite ⊕-identityʳ a | ⊕-identityˡ c = refl
⊕-assoc Z I c rewrite ⊕-identityˡ I = refl
⊕-assoc I I c rewrite ⊕-identityˡ c | ⊕-II c = refl

⊕-comm : (a b : Bit) → a ⊕ b ≡ b ⊕ a
⊕-comm Z b rewrite ⊕-identityʳ b | ⊕-identityˡ b = refl
⊕-comm I Z = refl
⊕-comm I I = refl

⊕-comm² : (a b c : Bit) → a ⊕ b ⊕ c ≡ b ⊕ a ⊕ c
⊕-comm² a b c = begin
  a ⊕ b ⊕ c    ≡⟨ ⊕-assoc a b c ⟩
  (a ⊕ b) ⊕ c  ≡⟨ cong (_⊕ c) $ ⊕-comm a b ⟩
  (b ⊕ a) ⊕ c  ≡⟨ sym (⊕-assoc b a c) ⟩
  b ⊕ a ⊕ c    ∎

⊕-elimˡ : (a b : Bit) → a ⊕ a ⊕ b ≡ b
⊕-elimˡ a b rewrite ⊕-assoc a a b | ⊕-elim a | ⊕-identityˡ b = refl

⊕-elimʳ : (a b : Bit) → a ⊕ b ⊕ b ≡ a
⊕-elimʳ a b rewrite ⊕-elim b | ⊕-identityʳ a = refl


⊕⨅-⨆ : (a b : Bit) → ⨆ (⨅ a b) (a ⊕ b) ≡ ⨆ a b
⊕⨅-⨆ Z Z = refl
⊕⨅-⨆ Z I = refl
⊕⨅-⨆ I Z = refl
⊕⨅-⨆ I I = refl

data CBin : Set
|b : CBin → Bit


data CBin where
  Z : CBin
  𝕔 : (p : CBin) → (b : Bit) → ⨆ (|b p) b ≡ I → CBin

|b Z = Z
|b (𝕔 c _ _) = I

|b-I : (a : CBin) → a ≢ Z → |b a ≡ I
|b-I Z nz = ⊥-elim (nz refl)
|b-I (𝕔 a b x) nz = refl

|b-Z : {a : CBin} → |b a ≡ Z → a ≡ Z
|b-Z {Z} refl = refl

inc-c : CBin → CBin
inc-c-|b : ∀ a → |b (inc-c a) ≡ I

inc-c Z = 𝕔 Z I refl
inc-c (𝕔 c Z x) = 𝕔 c I (⨆-Iʳ (|b c))
inc-c (𝕔 c I x) = 𝕔 (inc-c c) Z (inc-c-|b c)

inc-c-|b Z = refl
inc-c-|b (𝕔 a Z x) = refl
inc-c-|b (𝕔 a I x) = refl

inc-c≢Z : ∀ c → inc-c c ≢ Z
inc-c≢Z Z = λ ()
inc-c≢Z (𝕔 c Z x) = λ ()
inc-c≢Z (𝕔 c I x) = λ ()

+cit : Bit → CBin → CBin
+cit Z c = c
+cit I c = inc-c c

+citI-inc : (a : CBin) → +cit I a ≡ inc-c a
+citI-inc c = refl

+citZ-id : (a : CBin) → +cit Z a ≡ a
+citZ-id a = refl

+cit-|b : (b : Bit) (c : CBin) → |b (+cit b c) ≡ ⨆ b (|b c)
+cit-|b Z Z = refl
+cit-|b I Z = refl
+cit-|b Z (𝕔 _ _ _) = refl
+cit-|b I c@(𝕔 _ _ _) with inc-c c | inc-c≢Z c
...  | Z | nz = ⊥-elim $ nz refl
...  | 𝕔 cc b x | nz = refl

c…bit : CBin → Bit → CBin
c…bit Z Z = Z
c…bit Z I = 𝕔 Z I refl
c…bit c@(𝕔 _ _ p) b = 𝕔 c b (⨆-Iˡ b)

c…bit-|b : (a : CBin) (b : Bit) → |b (c…bit a b) ≡ ⨆ (|b a) b
c…bit-|b Z Z = refl
c…bit-|b Z I = refl
c…bit-|b (𝕔 _ _ _) Z = refl
c…bit-|b (𝕔 _ _ _) I = refl

c…bit-id : ∀ (a ab ap) → 𝕔 a ab ap ≡ c…bit a ab
c…bit-id Z I ap rewrite ≡-uniq refl ap = refl
c…bit-id (𝕔 a b x) Z ap rewrite ≡-uniq refl ap = refl
c…bit-id (𝕔 a b x) I ap rewrite ≡-uniq refl ap = refl

c+…-|b : (c : CBin) (a b : Bit) → |b (c…bit (+cit a c) b) ≡ ⨆ (⨆ a (|b c)) b
c+…-|b c a b rewrite c…bit-|b (+cit a c) b | +cit-|b a c = refl

data _≤ᶜ_ : CBin → CBin → Set where
  z  : {b : CBin} → Z ≤ᶜ b
  ≤… : {a b : CBin} → a ≤ᶜ b → (ab bb : Bit) → c…bit a ab ≤ᶜ c…bit b bb

data _<ᶜ_ : CBin → CBin → Set where
  z  : {b : CBin} → |b b ≡ I → Z <ᶜ b
  <… : {a b : CBin} → a <ᶜ b → (ab bb : Bit) → c…bit a ab <ᶜ c…bit b bb

_+ᶜ_ : CBin → CBin → CBin
Z +ᶜ b = b
a +ᶜ Z = a
𝕔 a ab ap +ᶜ 𝕔 b bb bp with ⨅ ab bb | ab ⊕ bb | a +ᶜ b
...  | cry | lsb | sum = c…bit (+cit cry sum) lsb

infixr 5 _+ᶜ_

|b-𝕔+ᶜ𝕔 : (a b : CBin) → |b (a +ᶜ b) ≡ ⨆ (|b a) (|b b)
|b-𝕔+ᶜ𝕔 Z Z = refl
|b-𝕔+ᶜ𝕔 Z b rewrite ⨆-Zˡ (|b b) = refl
|b-𝕔+ᶜ𝕔 a@(𝕔 _ _ _) Z rewrite ⨆-Zʳ (|b a) = refl
|b-𝕔+ᶜ𝕔 (𝕔 a ab ap) (𝕔 b bb bp) with a +ᶜ b | |b-𝕔+ᶜ𝕔 a b
...  | sum | |bsum = begin
  |b (c…bit (+cit (⨅ ab bb) sum) (ab ⊕ bb))  ≡⟨ c…bit-|b (+cit (⨅ ab bb) sum) (ab ⊕ bb) ⟩
  ⨆ (|b (+cit (⨅ ab bb) sum)) (ab ⊕ bb)      ≡⟨ cong (λ z → ⨆ z (ab ⊕ bb)) $ +cit-|b (⨅ ab bb) sum ⟩
  ⨆ (⨆ (⨅ ab bb) (|b sum)) (ab ⊕ bb)         ≡⟨ cong (λ z → ⨆ z (ab ⊕ bb)) $ ⨆-comm (⨅ ab bb) (|b sum) ⟩
  ⨆ (⨆ (|b sum) (⨅ ab bb)) (ab ⊕ bb)         ≡⟨ sym $ ⨆-assoc (|b sum) (⨅ ab bb) (ab ⊕ bb) ⟩
  ⨆ (|b sum) (⨆ (⨅ ab bb) (ab ⊕ bb))         ≡⟨ cong (⨆ (|b sum)) $ ⊕⨅-⨆ ab bb ⟩ -- ⨅⊕-⨆
  ⨆ (|b sum) (⨆ ab bb)                       ≡⟨ cong (λ z → ⨆ z (⨆ ab bb)) |bsum ⟩
  ⨆ (⨆ (|b a) (|b b)) (⨆ ab bb)              ≡⟨ sym $ ⨆-assoc ((|b a)) (|b b) (⨆ ab bb)  ⟩
  ⨆ (|b a) (⨆ (|b b) (⨆ ab bb))              ≡⟨ cong (⨆ (|b a)) $ ⨆-comm² (|b b) ab bb  ⟩
  ⨆ (|b a) (⨆ ab (⨆ (|b b) bb))              ≡⟨ cong (λ z → ⨆ (|b a) (⨆ ab z)) bp  ⟩
  ⨆ (|b a) (⨆ ab I)                          ≡⟨ cong (⨆ (|b a)) $ ⨆-Iʳ ab  ⟩
  ⨆ (|b a) I                                 ≡⟨ ⨆-Iʳ (|b a)  ⟩
  I  ∎

+ᶜ-comm : (a b : CBin) → a +ᶜ b ≡ b +ᶜ a
+ᶜ-comm Z Z = refl
+ᶜ-comm Z (𝕔 _ _ _) = refl
+ᶜ-comm (𝕔 _ _ _) Z = refl
+ᶜ-comm (𝕔 a ab ap) (𝕔 b bb bp) rewrite +ᶜ-comm a b | ⨅-comm ab bb | ⊕-comm ab bb = refl

+ᶜ-comm-λ : (F : CBin → CBin) → ((x y : CBin) → x +ᶜ F y ≡ F (x +ᶜ y)) → (a b : CBin) → F a +ᶜ b ≡ F (a +ᶜ b)
+ᶜ-comm-λ F F≡ a b rewrite +ᶜ-comm a b | +ᶜ-comm (F a) b = F≡ b a


+ᶜ-Zˡ : (b : CBin) → Z +ᶜ b ≡ b
+ᶜ-Zˡ Z = refl
+ᶜ-Zˡ (𝕔 _ _ _) = refl

+ᶜ-Zʳ : (a : CBin) → a +ᶜ Z ≡ a
+ᶜ-Zʳ Z = refl
+ᶜ-Zʳ (𝕔 _ _ _) = refl

+ᶜ1-inc : (a : CBin) → a +ᶜ 𝕔 Z I refl ≡ inc-c a
+ᶜ1-inc Z = refl
+ᶜ1-inc (𝕔 a Z ap) rewrite +ᶜ-Zʳ a | c…bit-id a I (⨆-Iʳ (|b a)) = refl
+ᶜ1-inc (𝕔 a I ap) = begin
  𝕔 a I ap +ᶜ 𝕔 Z I refl      ≡⟨⟩
  c…bit (inc-c (a +ᶜ Z)) Z    ≡⟨ cong (λ z → c…bit (inc-c z) Z ) $ +ᶜ-Zʳ a ⟩
  c…bit (inc-c a) Z           ≡⟨ sym (c…bit-id (inc-c a) Z (inc-c-|b a)) ⟩
  𝕔 (inc-c a) Z (inc-c-|b a)  ≡⟨⟩
  inc-c (𝕔 a I ap) ∎

inc-out : ∀ a → c…bit (inc-c a) Z ≡ inc-c (c…bit a I)
inc-out Z = refl
inc-out c@(𝕔 _ _ _) = begin
  c…bit (inc-c c) Z  ≡⟨ sym (c…bit-id (inc-c c) Z (inc-c-|b c )) ⟩
  𝕔 (inc-c c) Z (inc-c-|b c)  ≡⟨⟩
  inc-c (c…bit c I)  ∎

inc-… : ∀ a → c…bit a I ≡ inc-c (c…bit a Z)
inc-… Z = refl
inc-… (𝕔 a b x) = refl

+ᶜ-inc-c : (a b : CBin) → a +ᶜ inc-c b ≡ inc-c (a +ᶜ b)
+ᶜ-inc-c Z b = refl
+ᶜ-inc-c (𝕔 a ab ap) Z rewrite +ᶜ-Zʳ (𝕔 a ab ap) = +ᶜ1-inc (𝕔 a ab ap)
+ᶜ-inc-c (𝕔 a Z ap) (𝕔 b Z bp) = begin
  𝕔 a Z ap +ᶜ inc-c (𝕔 b Z bp)     ≡⟨⟩
  𝕔 a Z ap +ᶜ 𝕔 b I (⨆-Iʳ (|b b))  ≡⟨⟩
  c…bit (a +ᶜ b) (Z ⊕ I)           ≡⟨⟩
  c…bit (a +ᶜ b) I                 ≡⟨ inc-… (a +ᶜ b) ⟩
  inc-c (c…bit (a +ᶜ b) Z)         ∎ where
+ᶜ-inc-c (𝕔 a I ap) (𝕔 b Z bp) = begin
  𝕔 a I ap +ᶜ inc-c (𝕔 b Z bp)     ≡⟨⟩
  c…bit (inc-c (a +ᶜ b)) Z         ≡⟨ inc-out (a +ᶜ b) ⟩
  inc-c (c…bit (a +ᶜ b) I)         ∎ where
+ᶜ-inc-c (𝕔 a Z ap) (𝕔 b I bp) = begin
  𝕔 a Z ap +ᶜ inc-c (𝕔 b I bp)             ≡⟨⟩
  𝕔 a Z ap +ᶜ  𝕔 (inc-c b) Z (inc-c-|b b)  ≡⟨⟩
  c…bit (a +ᶜ inc-c b) Z                   ≡⟨ cong (λ z → c…bit z Z) $ +ᶜ-inc-c a b ⟩
  c…bit (inc-c (a +ᶜ b)) Z                 ≡⟨ inc-out (a +ᶜ b) ⟩
  inc-c (c…bit (a +ᶜ b) I)  ∎
+ᶜ-inc-c (𝕔 a I ap) (𝕔 b I bp) = begin
  𝕔 a I ap +ᶜ inc-c (𝕔 b I bp)      ≡⟨⟩
  c…bit (a +ᶜ inc-c b) I            ≡⟨ cong (λ z → c…bit z I) $ +ᶜ-inc-c a b ⟩
  c…bit (inc-c (a +ᶜ b)) I          ≡⟨ inc-… (inc-c (a +ᶜ b)) ⟩
  inc-c (c…bit (inc-c (a +ᶜ b)) Z)  ∎

+ᶜ-+cit : (a b : CBin) (bb : Bit) → a +ᶜ +cit bb b ≡ +cit bb (a +ᶜ b)
+ᶜ-+cit a b Z = refl
+ᶜ-+cit a b I rewrite +citI-inc b = +ᶜ-inc-c a b

+ᶜ-c…bit : ∀ a ab ap b lsb
  → 𝕔 a ab ap +ᶜ c…bit b lsb ≡ c…bit (+cit (⨅ ab lsb) (a +ᶜ b)) (ab ⊕ lsb)
+ᶜ-c…bit a ab ap Z Z rewrite +ᶜ-Zʳ (𝕔 a ab ap) | c…bit-id a ab ap | +ᶜ-Zʳ a | ⊕-identityʳ ab = refl
+ᶜ-c…bit a ab ap Z I rewrite sym $ c…bit-id Z I (⨆-Iʳ Z) = refl
+ᶜ-c…bit a ab ap b@(𝕔 _ _ _) lsb rewrite sym $ c…bit-id b lsb (⨆-Iˡ lsb) = refl

+ᶜ-assoc : (a b c : CBin) → a +ᶜ (b +ᶜ c) ≡ (a +ᶜ b) +ᶜ c
+ᶜ-assoc a b Z rewrite +ᶜ-Zʳ b  = sym $ +ᶜ-Zʳ (a +ᶜ b)
+ᶜ-assoc a Z c rewrite +ᶜ-Zˡ c = cong (_+ᶜ c) $ sym $ +ᶜ-Zʳ a
+ᶜ-assoc Z b c rewrite +ᶜ-Zˡ (b +ᶜ c) = refl
+ᶜ-assoc A@(𝕔 a ab ap) B@(𝕔 b bb bp) C@(𝕔 c cb cp) = begin
  A +ᶜ B +ᶜ C                                     ≡⟨⟩ --
  𝕔 a ab ap +ᶜ c…bit (+cit (⨅ bb cb) (b +ᶜ c)) (bb ⊕ cb)  ≡⟨ +ᶜ-assoc-lemma a ab ap b bb c cb ⟩

  c…bit (+cit (⨅ ab (bb ⊕ cb)) (+cit (⨅ bb cb) (a +ᶜ b +ᶜ c))) (ab ⊕ bb ⊕ cb)
  ≡⟨ cong (λ z → c…bit (+cit (⨅ ab (bb ⊕ cb)) (+cit (⨅ bb cb) z)) (ab ⊕ bb ⊕ cb)) (+ᶜ-assoc a b c) ⟩

  c…bit (+cit (⨅ ab (bb ⊕ cb)) (+cit (⨅ bb cb) ((a +ᶜ b) +ᶜ c))) (ab ⊕ bb ⊕ cb)
  ≡⟨ cong (λ z → c…bit z (ab ⊕ bb ⊕ cb)) (+cit-swap ab bb cb ((a +ᶜ b) +ᶜ c)) ⟩

  c…bit (+cit (⨅ (ab ⊕ bb) cb) (+cit (⨅ ab bb) ((a +ᶜ b) +ᶜ c))) (ab ⊕ bb ⊕ cb)
  ≡⟨ cong (c…bit (+cit (⨅ (ab ⊕ bb) cb) (+cit (⨅ ab bb) ((a +ᶜ b) +ᶜ c)))) (⊕-assoc ab bb cb) ⟩

  c…bit (+cit (⨅ (ab ⊕ bb) cb) (+cit (⨅ ab bb) ((a +ᶜ b) +ᶜ c))) ((ab ⊕ bb) ⊕ cb)
  ≡⟨ cong (λ z → c…bit (+cit (⨅ (ab ⊕ bb) cb) z) ((ab ⊕ bb) ⊕ cb)) (+cit-+ᶜ (a +ᶜ b) c (⨅ ab bb)) ⟩

  c…bit (+cit (⨅ (ab ⊕ bb) cb) (+cit (⨅ ab bb) (a +ᶜ b) +ᶜ c)) ((ab ⊕ bb) ⊕ cb)
  ≡⟨ c…bit-+ᶜ (+cit (⨅ ab bb) (a +ᶜ b)) (ab ⊕ bb) c cb cp ⟩

  c…bit (+cit (⨅ ab bb) (a +ᶜ b)) (ab ⊕ bb) +ᶜ C
  ≡⟨⟩

  (A +ᶜ B) +ᶜ C  ∎ where

  +ᶜ-assoc-lemma : ∀ a ab ap b bb c cb
    → 𝕔 a ab ap +ᶜ c…bit (+cit (⨅ bb cb) (b +ᶜ c)) (bb ⊕ cb) ≡
      c…bit (+cit (⨅ ab (bb ⊕ cb)) (+cit (⨅ bb cb) (a +ᶜ b +ᶜ c))) (ab ⊕ bb ⊕ cb)
  +ᶜ-assoc-lemma  a ab ap b bb c cb = begin
    𝕔 a ab ap +ᶜ c…bit (+cit (⨅ bb cb) (b +ᶜ c)) (bb ⊕ cb)
    ≡⟨ +ᶜ-c…bit a ab ap (+cit (⨅ bb cb) (b +ᶜ c)) (bb ⊕ cb) ⟩

    c…bit (+cit (⨅ ab (bb ⊕ cb)) (a +ᶜ +cit (⨅ bb cb) (b +ᶜ c)) ) (ab ⊕ bb ⊕ cb)
    ≡⟨ cong (λ z → c…bit (+cit (⨅ ab (bb ⊕ cb)) z ) (ab ⊕ bb ⊕ cb)) (+ᶜ-+cit a (b +ᶜ c) (⨅ bb cb)) ⟩

    c…bit (+cit (⨅ ab (bb ⊕ cb)) (+cit (⨅ bb cb) (a +ᶜ b +ᶜ c))) (ab ⊕ bb ⊕ cb)
    ∎
  +cit-swap : ∀ ab bb cb c
    → +cit (⨅ ab (bb ⊕ cb)) (+cit (⨅ bb cb) c) ≡ +cit (⨅ (ab ⊕ bb) cb) (+cit (⨅ ab bb) c)
  +cit-swap Z Z Z c = refl
  +cit-swap I I I c = refl
  +cit-swap Z Z I c = refl
  +cit-swap Z I Z c = refl
  +cit-swap Z I I c = refl
  +cit-swap I Z Z c = refl
  +cit-swap I Z I c = refl
  +cit-swap I I Z c = refl
  +cit-+ᶜ : (a b : CBin) (ab : Bit) → +cit ab (a +ᶜ b) ≡ +cit ab a +ᶜ b
  +cit-+ᶜ a b ab rewrite
      +ᶜ-comm a b
    | +ᶜ-comm (+cit ab a) b
    = sym (+ᶜ-+cit b a ab)
  c…bit-+ᶜ : ∀ a ab b bb bp
    → c…bit (+cit (⨅ ab bb) (a +ᶜ b)) (ab ⊕ bb) ≡ c…bit a ab +ᶜ 𝕔 b bb bp
  c…bit-+ᶜ a ab b bb bp rewrite
       ⨅-comm ab bb
    |  ⊕-comm ab bb
    | +ᶜ-comm a  b
    | +ᶜ-comm (c…bit a ab) (𝕔 b bb bp)
    = sym (+ᶜ-c…bit b bb bp a ab)