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.

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