Cauchy real numbers

[lowasser]

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 is the analytic limited principle of omniscience and how trichotomy of the standard ordering on Cauchy (but not Dedekind) real numbers is equivalent to the standard LPO on the natural numbers.

This has several subtasks, which I'll attempt to add as sub-issues.