zeroᴮ : Can (⟨⟩ O)

  zero-bin : Can (⟨⟩ O)

inc-can zeroᴮ = leading one

inc-can zero-bin = leading one

to-can zero = zeroᴮ

to-can zero = zero-bin

∀-distrib-×' : ∀ {A : Set} {B C : A → Set} →
  (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
∀-distrib-×' = record
  { to = λ a→b×c → ⟨ proj₁ ∘ a→b×c , proj₂ ∘ a→b×c ⟩
  ; from = λ a→b×a→c a → ⟨ proj₁ a→b×a→c a , proj₂ a→b×a→c a ⟩
  ; from∘to = λ _ → refl
  ; to∘from = λ _ → refl
  }
→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× = ∀-distrib-×'

⊎∀-implies-∀⊎' : ∀ {A : Set} {B C : A → Set} →
  (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
⊎∀-implies-∀⊎' (inj₁ a→b) a = inj₁ (a→b a)
⊎∀-implies-∀⊎' (inj₂ a→c) a = inj₂ (a→c a)

tri-b-iso-b-× : ∀ {B : Tri → Set} → (∀ (x : Tri) → B x) ≃ B aa × B bb × B cc
tri-b-iso-b-× = record
  { to = λ to-b → ⟨ to-b aa , ⟨ to-b bb , to-b cc ⟩ ⟩
  ; from = λ aabbcc → λ
    { aa → proj₁ aabbcc
    ; bb → (proj₁ ∘ proj₂) aabbcc
    ; cc → (proj₂ ∘ proj₂) aabbcc
    }
  ; from∘to = λ _ → ∀-extensionality λ { aa → refl ; bb → refl ; cc → refl }
  ; to∘from = λ _ → refl
  }

open Eq.≡-Reasoning
open Eq using (cong;sym)
open import Data.Nat.Properties using (+-identityʳ;+-comm;+-assoc)
∃-even' : ∀ {n : ℕ} → ∃[ m ] (    2 * m ≡ n) → even n
∃-odd'  : ∀ {n : ℕ} → ∃[ m ] (2 * m + 1 ≡ n) →  odd n
∃-even' ⟨ zero , refl ⟩ = even-zero
∃-even' ⟨ suc m , refl ⟩ with even-suc (∃-odd' ⟨ m , refl ⟩)
...| n rewrite +-identityʳ m | +-assoc m m 1 | +-comm m 1 = n
∃-odd' ⟨ m , refl ⟩ with ∃-even' ⟨ m , refl ⟩
...| n rewrite +-comm (m + (m + 0)) 1 = odd-suc n

open import plfa.part1.Isomorphism using (_⇔_)
open Data.Nat using (_≤_; z≤n; s≤s; _∸_)
open Data.Nat.Properties using (≤-refl;∸-monoˡ-≤)
≡→≤ : {a b : ℕ} → a ≡ b → a ≤ b
≡→≤ refl = ≤-refl
b≤b+a : {a b : ℕ} → b ≤ b + a
b≤b+a {zero} {zero} = z≤n
b≤b+a {zero} {suc b} rewrite +-identityʳ b = s≤s ≤-refl
b≤b+a {suc a} {zero} = z≤n
b≤b+a {suc a} {suc b} = s≤s b≤b+a
+≡→≤ : {a b c : ℕ} → suc (a + b) ≡ c → b ≤ c
+≡→≤ {b = zero} refl = z≤n
+≡→≤ {a = zero} {b = suc b} refl = s≤s (+≡→≤ refl)
+≡→≤ {a = suc a} {b = suc b} refl
  rewrite +-comm 1 (a + suc b)
        | +-comm a (suc b)
        | +-comm 1 (b + a + 1)
        | +-assoc (b + a) 1 1
        | +-assoc b a 2 = s≤s b≤b+a
n∸m+suc-m≡suc-n : {a b : ℕ} → b ≤ a → a ∸ b + suc b ≡ suc a
n∸m+suc-m≡suc-n {zero} {zero} z≤n = refl
n∸m+suc-m≡suc-n {zero} {suc b} ()
n∸m+suc-m≡suc-n {suc a} {zero} z≤n rewrite +-comm a 1 = refl
n∸m+suc-m≡suc-n {suc a} {suc b} (s≤s b≤a)
  rewrite +-comm 1 (suc b)
        | +-comm 1 (suc a)
        | +-comm (a ∸ b) (suc (b + 1))
        | +-comm (b + 1) (a ∸ b)
        | +-comm b 1
        | +-comm a 1 = cong (λ x → 1 + x) (n∸m+suc-m≡suc-n {a} {b} b≤a)
∃-+-≤ : ∀ { y z : ℕ } → (∃[ x ] (x + y ≡ z)) ⇔ (y ≤ z)
∃-+-≤ {y} {z} = record
  { to = λ { ⟨ zero , y≡z ⟩ → ≡→≤ y≡z ; ⟨ suc x , suc-x+y≡z ⟩ → +≡→≤ suc-x+y≡z }
  ; from = λ { z≤n → ⟨ (z ∸ y) , (+-identityʳ  z) ⟩ ; (s≤s m≤n) → ⟨ (z ∸ y) , n∸m+suc-m≡suc-n m≤n ⟩ }
  }

∃¬-implies-¬∀' : ∀ {A : Set} {B : A → Set}
  → ∃[ x ] (¬ B x)
  → ¬ (∀ x → B x)
∃¬-implies-¬∀' ⟨ a , ¬Bx ⟩ = λ x→Bx → ¬Bx (x→Bx a)

open import plfa.part1.Relations using (Bin; to; from; inc; One; Can; to-can; inc-can; from-inc-suc-from)
-- from plfa.part1.Induction
postulate
  from-to-id : ∀ (m : ℕ) → from (to m) ≡ m
  proj₁≡→Can≡ : {c c′ : ∃[ b ] Can b} → Σ.proj₁ c ≡ Σ.proj₁ c′ → c ≡ c′
  can-to-from-id : ∀ {b : Bin} → Can b → to (from b) ≡ b
-- NOTE: Not sure why this fails with TerminationIssue, so I postulate it above instead
-- can-to-from-id : ∀ {b : Bin} → Can b → to (from b) ≡ b
-- can-to-from-id Can.zero-bin = refl
-- can-to-from-id (Can.leading One.one) = refl
-- can-to-from-id (Can.leading (One.suc {b} o)) =
--   begin
--     to (from (inc b))
--   ≡⟨ cong to (from-inc-suc-from b) ⟩
--     to (suc (from b))
--   ≡⟨ cong inc (can-to-from-id (Can.leading o)) ⟩
--     inc b
--   ∎
ℕ-≃-can : ℕ ≃ (∃[ b ] Can b)
ℕ-≃-can = record
  { to = λ n → ⟨ to n , to-can n ⟩
  ; from = λ (⟨ b , can ⟩) → from b
  ; from∘to = λ n → from-to-id n
  ; to∘from = λ (⟨ b , can ⟩) → proj₁≡→Can≡ (can-to-from-id can)
  }