postulate
  ≃-implies-≲ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≲ B

-- postulate
--   ≃-implies-≲ : ∀ {A B : Set}
--     → A ≃ B
--       -----
--     → A ≲ B

≃-implies-≲ : ∀ {A B : Set}
  → A ≃ B
    -----
  → A ≲ B
≃-implies-≲ A≅B =
  record
  { to = to A≅B
  ; from = from A≅B
  ; from∘to = from∘to A≅B
  }

module ⇔-exer where
  open _⇔_
  ⇔-refl : ∀ {A : Set} → A ⇔ A
  ⇔-refl = record
    { to =   λ a → a
    ; from = λ a → a
    }
  ⇔-sym : ∀ {A B : Set} → A ⇔ B → B ⇔ A
  ⇔-sym = λ A⇔B → record
    { to = from A⇔B
    ; from = to A⇔B
    }
  ⇔-trans : ∀ {A B C : Set} → A ⇔ B → B ⇔ C → A ⇔ C
  ⇔-trans A⇔B B⇔C = record
    { to =   λ a → to B⇔C   (to A⇔B a)
    ; from = λ c → from A⇔B (from B⇔C c)
    }

open Data.Nat.Base using (_*_)
open Data.Nat.Properties using (*-comm;+-assoc)
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (rest O) = rest I
inc (rest I) = (inc rest) O
toᴮ   : ℕ → Bin
toᴮ zero = ⟨⟩ O
toᴮ (suc n) = inc (toᴮ n)
fromᴮ : Bin → ℕ
fromᴮ ⟨⟩ = 0
fromᴮ (rest O) = 2 * (fromᴮ rest)
fromᴮ (rest I) = 1 + 2 * (fromᴮ rest)
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl
from-inc-suc-from : ∀ (b : Bin) → fromᴮ (inc b) ≡ suc (fromᴮ b)
from-inc-suc-from ⟨⟩ = refl
from-inc-suc-from (b O) = refl
from-inc-suc-from (b I) =
  begin
    fromᴮ (inc (b I))
  ≡⟨⟩
    fromᴮ ((inc b) O)
  ≡⟨⟩
    2 * (fromᴮ (inc b))
  ≡⟨ cong (\x → 2 * x) (from-inc-suc-from b) ⟩
    2 * suc (fromᴮ b)
  ≡⟨⟩
    2 * (1 + (fromᴮ b))
  ≡⟨ *-comm 2 (1 + (fromᴮ b)) ⟩
    (1 + (fromᴮ b)) * 2
  ≡⟨ *-distrib-+ 1 (fromᴮ b) 2 ⟩
    2 + (fromᴮ b) * 2
  ≡⟨ cong (\x → 2 + x) (*-comm (fromᴮ b) 2) ⟩
    2 + 2 * (fromᴮ b)
  ≡⟨⟩
    suc (1 + 2 * (fromᴮ b))
  ≡⟨⟩
    suc (fromᴮ (b I))
  ∎
fromᴮ∘toᴮ : ∀ (n : ℕ) → (fromᴮ ∘ toᴮ) n ≡ n
fromᴮ∘toᴮ zero = refl
fromᴮ∘toᴮ (suc n) =
  begin
    (fromᴮ ∘ toᴮ) (suc n)
  ≡⟨⟩
    fromᴮ (toᴮ (suc n))
  ≡⟨⟩
    fromᴮ (inc (toᴮ n))
  ≡⟨ from-inc-suc-from (toᴮ n) ⟩
    suc (fromᴮ (toᴮ n))
  ≡⟨ cong suc (fromᴮ∘toᴮ n) ⟩
    suc n
  ∎
ℕ-≲-Bin : ℕ ≲ Bin
ℕ-≲-Bin = record
  { to = toᴮ
  ; from = fromᴮ
  ; from∘to = fromᴮ∘toᴮ
  }

  Because a non-zero Bin that starts with zeros will have the leading zeros stripped