[Agda] Komencenta demando.

[Matteo Acerbi]

On Wed, Mar 2, 2016 at 3:58 PM, Serge Leblanc <33dbqnxpy7if at gmail.com> wrote:
> Dear all,
>
> I'm trying to prove bijection between ℕ × ℕ and ℕ. Due to  (ℕ × ℕ) not
> decrease, I fail to proof it.
> [..]

If you're interested, this is how I approached this exercise a while ago:

https://gist.github.com/ma82/ceab499710fecf90eda2

As the name suggests, I used the Bove-Capretta method.

There surely are other approaches, also based on other pairing
functions (e.g. pair :: Natural -> Natural -> Natural from
http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/).

Cheers,
Matteo

PS. I didn't check the file still works, I haven't had time to compile
Agda in months.