Louis Wasserman

Untruncate uniform continuity

22

This comes back to similar reasons to why we can't truncate the modulus of convergence of sequences and the like: we need to actually calculate convergence rates. I'm specifically running...

The Dedekind real numbers are the standard definition used in agda-unimath, but the Cauchy real numbers have some neat properties worth exploring; the one that immediately comes to my mind...

In service of #1455, we can make the Cauchy real numbers support arithmetic, inequality, etc. even if we can't necessarily prove they're complete. Multiplication on Cauchy real numbers should be...

Initial semiring of natural numbers

3

We have that Z is the initial ring, but not that N is the initial semiring. I've started to tackle this, but it is unexpectedly complicated; I've notably run into...

Simplifications for Theorem 11.2.12 {RD-cauchy-complete}

2

While implementing this result in agda-unimath (https://github.com/UniMath/agda-unimath/pull/1343), I came across a few simplifications to the current proof. I'll go in order of the things I'd change, which is coincidentally *ascending*...