单值基础中的域理论 I：有向完备偏序集与 Scott 的 $D_\infty$
Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$
AI总结：
本文在构造性和谓词性单值基础中发展域理论，通过跟踪类型宇宙参数实现有向完备偏序集的迭代构造，并给出 Scott 的 $D_\infty$ 模型的谓词性重构，已在 Agda 中形式化。
摘要：
我们在构造性和谓词性的单值基础（也称为同伦类型论）中发展域理论。谓词性工作意味着我们不假设 Voevodsky 的命题重缩公理。我们的工作是构造性的，即我们不依赖排中律或（可数）选择公理。域理论研究所谓的有向完备偏序集（dcpos）及其之间的 Scott 连续映射，并在编程语言语义、高阶可计算性和拓扑学等领域有广泛应用。在谓词性基础中处理大小问题的常见方法是使用信息系统、抽象基或形式拓扑而非 dcpos，以及使用逼近关系而非 Scott 连续函数。在我们的类型论方法中，我们转而接受 dcpos 可能是大的，并使用类型宇宙来应对这一点。先验地，人们可能期望 dcpos 的迭代构造可能导致对不断增大的宇宙的需求，并且在谓词性上是不可能的。我们通过仔细跟踪类型宇宙参数，展示了此类构造可以在谓词性环境中进行。特别是，我们给出了无类型 $\lambda$-演算的 Scott 的 $D_\infty$ 模型的谓词性重构。我们的工作已在 Agda 证明助手中形式化，其推断宇宙层级的能力对我们的目的而言是无价的。
英文摘要：
We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsky's propositional resizing axioms. Our work is constructive in the sense that we do not rely on excluded middle or the axiom of (countable) choice. Domain theory studies so-called directed complete posets (dcpos) and Scott continuous maps between them and has applications in a variety of fields, such as programming language semantics, higher-type computability and topology. A common approach to deal with size issues in a predicative foundation is to work with information systems, abstract bases or formal topologies rather than dcpos, and approximable relations rather than Scott continuous functions. In our type-theoretic approach, we instead accept that dcpos may be large and work with type universes to account for this. A priori one might expect that iterative constructions of dcpos may result in a need for ever-increasing universes and are predicatively impossible. We show, through a careful tracking of type universe parameters, that such constructions can be carried out in a predicative setting. In particular, we give a predicative reconstruction of Scott's $D_\infty$ model of the untyped $λ$-calculus. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
