https://plfa.github.io/Relations/#Bin-predicates

Bin.agda

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Function.Base
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties
open import Data.Sum

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (b O) = b I
inc (b I) = (inc b) O

data One : Bin → Set where
  ⟨1⟩ : One (⟨⟩ I)
  _O : ∀ {b : Bin} → One b → One (b O)
  _I : ∀ {b : Bin} → One b → One (b I)

data Can : Bin → Set where
  ⟨O⟩ : Can (⟨⟩ O)
  C : ∀ {b : Bin} → One b → Can b

inc-one : {b : Bin} → One b → One (inc b)
inc-one {.(⟨⟩ I)} ⟨1⟩ = ⟨1⟩ O
inc-one {.(_ O)} (o O) = o I
inc-one {.(_ I)} (o I) = inc-one o O

inc-can : {b : Bin} → Can b → Can (inc b)
inc-can {.(⟨⟩ O)} ⟨O⟩ = C ⟨1⟩
inc-can {b} (C x) = C (inc-one x)

to : ℕ → Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)

from : Bin → ℕ
from ⟨⟩ = 0
from (b O) = from b * 2
from (b I) = suc (from b * 2)

to-*2 : {n : ℕ} → (n ≢ 0) → to (n * 2) ≡ (to n) O
to-*2 {zero} n≢0 = ⊥-elim (n≢0 refl)
to-*2 {suc zero} _ = refl
to-*2 {suc (suc n)} _ = cong (inc ∘ inc) (to-*2 {suc n} 1+n≢0)

one≢0 : {b : Bin} → One b → from b ≢ 0
one≢0 ⟨1⟩ = 1+n≢0
one≢0 {b O} (o O) h with m*n≡0⇒m≡0∨n≡0 (from b) h
...                 | inj₁ x = one≢0 o x
one≢0 {b I} (o I) = 1+n≢0

one-Bin→ℕ→Bin : {b : Bin} → One b → to (from b) ≡ b
one-Bin→ℕ→Bin {(⟨⟩ I)} ⟨1⟩ = refl
one-Bin→ℕ→Bin {(b O)} (c O) =
    to (from b * 2)
  ≡⟨ to-*2 {from b} (one≢0 c) ⟩
    to (from b) O
  ≡⟨ cong _O (one-Bin→ℕ→Bin {b} c) ⟩
    b O
  ∎
one-Bin→ℕ→Bin {(b I)} (c I) =
    inc (to (from b * 2))
  ≡⟨ cong inc (to-*2 {from b} (one≢0 c)) ⟩
    inc (to (from b) O)
  ≡⟨ cong (inc ∘ _O) (one-Bin→ℕ→Bin {b} c) ⟩
    b I
  ∎

can-Bin→ℕ→Bin : {b : Bin} → Can b → to (from b) ≡ b
can-Bin→ℕ→Bin {.(⟨⟩ O)} ⟨O⟩ = refl
can-Bin→ℕ→Bin {b} (C x) = one-Bin→ℕ→Bin x

from-+1 : {b : Bin} → from (inc b) ≡ suc (from b)
from-+1 {⟨⟩} = refl
from-+1 {b O} = refl
from-+1 {b I} = cong (_* 2) (from-+1 {b})

ℕ→Bin→ℕ : {n : ℕ} → from (to n) ≡ n
ℕ→Bin→ℕ {zero} = refl
ℕ→Bin→ℕ {suc n} = trans (from-+1 {to n}) (cong suc ℕ→Bin→ℕ)