  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.
