Continuous and algebraic domains in univalent foundations

TL;DR

This paper develops a constructive, predicative theory of continuous and algebraic domains within univalent foundations, avoiding classical axioms and formalizing the results in Agda.

Contribution

It introduces a predicative, constructive framework for domain theory in univalent foundations, including definitions of continuity and bases without classical axioms.

Findings

Scott's D_infinity model is an algebraic dcpo with a small basis.

Continuous dcpos with small bases are exactly those presented by small ideals.

The theory is formalized in Agda, leveraging universe level inference.

Abstract

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.