standard bijections of Natural numbers

[Freek98]

Added proofs showing that the type of natural numbers is isomorphic to it's own sum and product.

• Showed that if we have a function $f : \mathbb N \to \mathbb N$, which is increasing and starts at 0. We can then partition $\mathbb N$ into the pieces $[f k , f(k+1) )$.
• Applying this fun fact to the double function, derived that $\mathbb N \cong \mathbb N + \mathbb N$
• Applying this fun fact to the function ($n \mapsto \frac{n (n+1)}{2} $), derived that $\mathbb N \cong \mathbb N \times \mathbb N$.
• There are also some small lemmas on the order of natural numbers and increasing functions.

[ecavallo]

This looks more like Triangle⊂ℕ×ℕ to me.

[ecavallo]

I changed Triangle⊂ℕ≅ℕ×ℕ to match. Merging now!

[anshwad10]

Looks like you could use totalEquiv from Cubical.Functions.Fibration here (as n ≤ m is definitionally the same as fiber (_+ n) m)

[anshwad10]

The solver here is also overkill, considering that this is exactly the type of +-suc

[anshwad10]

This is doubleℕ which is already defined in the library

[anshwad10]

This is also an instance of +-comm or +-suc, the solver is overkill

[anshwad10]

There is a lot of unnecessary whitespace between these lines
Also if you swap the positions of n and k here, you can use J>_ to simplify the proof a bit and avoid having to explicitly use subst

[anshwad10]

Well, I had some nitpciks, but seems im too late because its already merged