Kata

We have:

data Painfulℕ : Set where
  pain : ∀ zero? → (zero? ≡ false → Painfulℕ) → Painfulℕ

The first parameter of a constructor pain indicates whether current value is zero. The second parameter is a function which makes sure that current value is not zero and returns a predecessor of that value.

Your task is to write some operations on Painfulℕ, and proofs that require functional extensionality(and UIP in Coq)!

In bonus, show bijection between natural numbers and their painful version.

Note: Preloaded is using custom definition of bijection:

record _⇔_ (A B : Set) : Set where
  constructor Bijection
  field
    to      : A → B
    from    : B → A
    to∘from : ∀ x → to (from x) ≡ x
    from∘to : ∀ x → from (to x) ≡ x

If you want to do it in your text editor, here's the version to copy-paste: OwO