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 $\lambda$-calculus. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.

翻译：我们在构造性与谓词性单值基础（亦称同伦类型论）中发展域论。谓词性工作意味着我们不假设沃耶沃茨基的命题重设公理。我们的工作是构造性的，即不依赖于排中律或（可数）选择公理。域论研究所谓的定向完备偏序集（dcpos）及其间的斯科特连续映射，在编程语言语义学、高阶可计算性与拓扑学等多个领域具有应用。在谓词性基础中处理规模问题的常见方法是使用信息系统、抽象基或形式拓扑而非 dcpos，以及可逼近关系而非斯科特连续函数。在我们的类型论方法中，我们转而接受 dcpos 可能是大类型，并通过类型宇宙来处理这一问题。先验地，人们可能预期 dcpos 的迭代构造会导致对不断增大的宇宙的需求，从而在谓词性框架下不可行。我们通过对类型宇宙参数的精细追踪，证明了此类构造可以在谓词性设置中实现。特别地，我们给出了无类型 $\lambda$-演算的斯科特 $D_\infty$ 模型的谓词性重构。我们的工作已在 Agda 证明助手中形式化，其推断宇宙层级的能力对我们的研究至关重要。