agda-metric-reals

This is all work in progress, but here's the table of contents / plan / aspirations:

• "Upper" real numbers, defined as closed upper subsets of positive rationals upper-reals
  • Each number is represented similarly to an upper Dedekind cut
  • These form a semiring and a complete lattice
• Metric spaces, with distances valued in the upper reals metric2/base
  • Form a category with non-expansive maps as morphisms
  • This category has a terminal object metric2/terminal.
  • It has binary products metric2/product, with distances given by maximum.
  • It has another monoidal structure metric2/monoidal, with distance given by addition, which is closed metric2/internal-hom.
  • It has a graded "scaling" comonad, which allows the expression of all Lipschitz continuous functions by making their Lipschitz constant explicit metric2/scaling.
  • It has a completion monad, which completes a metric space by adding all limit points metric2/completion. This is implemented using regular functions as in Russell O'Connor's work (see references below).
  • The rationals form a metric space metric2/rationals, whose completion is the (full) real numbers. This is mostly unfinished.
  • It has a monad of convex combinations metric2/convex-alg, i.e. a probability distribution monad. The basic idea follows the Quantitative Algebraic Theories of Mardare, Panangaden and Plotkin. This should allow an integration operator, following the work of O'Connor and Spitters.

The Agda files are being developed with Agda 2.6.1 and standard library 1.6.

References

• Russell O'Connor: A monadic, functional implementation of real numbers. Math. Struct. Comput. Sci. 17(1): 129-159 (2007)
• Russell O'Connor, Bas Spitters: A computer-verified monadic functional implementation of the integral. Theor. Comput. Sci. 411(37): 3386-3402 (2010)
• Radu Mardare, Prakash Panangaden, Gordon D. Plotkin: Quantitative Algebraic Reasoning. LICS 2016: 700-709