agda-metric-reals

agda-metric-reals 这一切都在进行中，但这是目录/计划/愿望： “上”实数，定义为正有理封闭上子集 每个数字的表示方式都类似于上Dedekind切口 这些形成一个半环和一个完整的晶格 度量空间，其距离的值以较高的实数 用非膨胀图作为态射形成一个类别 此类别具有一个终端对象 。 它具有二进制乘积 ，其距离由最大值给出。 它具有另一个结构，其距离由加法给出，是封闭的 。 它具有分级的“缩放”符号，通过使Lipschitz恒定的明确的常数，可以表达所有Lipschitz连续函数。 它具有一个完成单子，该单子通过添加所有极限点来完成一个度量空间。 这是使用Russell O'Connor的工作中的常规函数​​实现的（请参见下面的参考资料）。 有理数形成一个度量空间 ，其完成是（完整的）实数。 这主要是未完成的。 它具有凸组合单子，即概率分布单子。 基本思想遵循马尔代