We develop the theory of continuous and algebraic domains in constructive and predicative univalent foundations, building upon our earlier work on basic domain theory in this setting. 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. To deal with size issues and give a predicatively suitable definition of continuity of a dcpo, we follow Johnstone and Joyal's work on continuous categories. Adhering to the univalent perspective, we explicitly distinguish between data and property. To ensure that being continuous is a property of a dcpo, we turn to the propositional truncation, although we explain that some care is needed to avoid needing the axiom of choice. We also adapt the notion of a domain-theoretic basis to the predicative setting by imposing suitable smallness conditions, analogous to the categorical concept of an accessible category. All our running examples of continuous dcpos are then actually examples of dcpos with small bases which we show to be well behaved predicatively. In particular, such dcpos are exactly those presented by small ideals. As an application of the theory, we show that Scott's $D_\infty$ model of the untyped $\lambda$-calculus is an example of an algebraic dcpo with a small basis. Our work is formalised in the Agda proof assistant and its ability to infer universe levels has been invaluable for our purposes.

翻译：我们在构造性与直谓性单值基础中发展了连续域与代数域的理论，这建立在我们先前在此背景下关于基本域论的研究之上。我们采用直谓性意味着我们并不假设Voevodsky的命题重设公理。我们的工作是构造性的，即不依赖于排中律或（可数）选择公理。为了处理规模问题并给出直谓意义上合适的dcpo连续性定义，我们遵循了Johnstone与Joyal关于连续范畴的研究。遵循单值观点，我们明确区分数据与性质。为确保连续性成为dcpo的性质，我们转向命题截断，尽管我们解释了需要谨慎处理以避免依赖选择公理。我们还通过施加适当的小性条件（类似于可及范畴的范畴论概念），将域论基的概念适配到直谓性框架中。我们所有连续dcpo的运行实例实际上都是具有小基的dcpo示例，我们证明了它们在直谓框架下具有良好的性质。特别地，这类dcpo恰好可由小理想表示。作为该理论的应用，我们证明了Scott的无类型$\lambda$演算$D_\infty$模型是具有小基的代数dcpo的实例。我们的工作已在Agda证明助手中形式化，其推断宇宙层级的能力对我们的研究具有重要价值。