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 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 complex constructions of dcpos result in a need for ever-increasing universes and are predicatively impossible. We show that such constructions can be carried out in a predicative setting. We illustrate the development with applications in the semantics of programming languages: the soundness and computational adequacy of the Scott model of PCF and Scott's $D_\infty$ model of the untyped $\lambda$-calculus. We also give a predicative account of continuous and algebraic dcpos, and of the related notions of a small basis and its rounded ideal completion. The fact that nontrivial dcpos have large carriers is in fact unavoidable and characteristic of our predicative setting, as we explain in a complementary chapter on the constructive and predicative limitations of univalent foundations. Our account of domain theory in univalent foundations is fully formalised with only a few minor exceptions. The ability of the proof assistant Agda to infer universe levels has been invaluable for our purposes.

翻译：我们在构造性和可判定幺半群基础（也称为同伦类型论）中发展域理论。采用可判定性意味着我们不假定Voevodsky的命题缩放公理。我们的工作具有构造性，即不依赖排中律或（可数）选择公理。域理论研究所谓的定向完备偏序集（dcpo）及其上的斯科特连续映射，并应用于编程语言语义、高阶可计算性和拓扑学。在可判定性基础中处理大小问题的常见方法是使用信息系统、抽象基或形式拓扑而非dcpo，以及使用可逼近关系而非斯科特连续函数。在我们的类型论方法中，我们接受dcpo可能规模较大，并通过类型宇宙来应对这一情况。从先验角度看，人们可能预期dcpo的复杂构造会导致宇宙层级不断上升，且无法在可判定性框架中实现。我们证明此类构造可以在可判定性设定下完成。我们通过编程语言语义中的两个应用案例进行说明：PCF的斯科特模型及无类型λ演算的斯科特$D_\infty$模型的声音性与计算充分性。我们还给出了连续和代数dcpo及其相关概念（小基与带舍入的理想完备化）的可判定性描述。正如我们在关于幺半群基础构造性与可判定性局限性的补充章节中所述，非平凡dcpo必然具有大载体的这一事实在我们的可判定性背景下是不可避免且具有特征性的。我们对幺半群基础中域理论的阐述已完全形式化（仅极少数例外）。证明助手Agda推断宇宙层级的能力对我们的目标具有不可估量的价值。