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）及其上的Scott连续映射，在编程语言语义学、高阶可计算性与拓扑学中具有应用。在预测性基础中处理规模问题的常用方法是采用信息系统、抽象基或形式拓扑替代dcpo，并使用可逼近关系替代Scott连续函数。在我们的类型论方法中，我们接受dcpo可能为大结构，并通过类型宇宙来处理这一问题。先验地，人们可能预期dcpo的复杂构造会导致不断增大的宇宙需求，从而在预测性框架中不可行。我们证明此类构造可在预测性设定中实现。我们通过编程语言语义学中的两个应用来阐释该发展：PCF的Scott模型的可靠性与计算充分性，以及无类型λ-演算的Scott $D_\infty$ 模型。我们还给出了连续与代数dcpo、及其相关的小基与圆整理想完备化概念的预测性阐释。正如在关于单值基础构造性与预测性局限性的补充章节中所解释的，非平凡dcpo具有大载体的事实是不可避免的，且这正是我们预测性设定的特征。我们对单值基础中域论的阐述已完全形式化，仅有少量例外。证明助手Agda对宇宙层次的推理能力对我们的目标而言至关重要。