  We develop domain theory in constructive univalent foundations without
Voevodsky's resizing axioms. In previous work in this direction, we constructed
the Scott model of PCF and proved its computational adequacy, based on directed
complete posets (dcpos). Here we further consider algebraic and continuous
dcpos, and construct Scott's $D_\infty$ model of the untyped
$\lambda$-calculus. A common approach to deal with size issues in a predicative
foundation is to work with information systems or abstract bases or formal
topologies rather than dcpos, and approximable relations rather than Scott
continuous functions. Here we instead accept that dcpos may be large and work
with type universes to account for this. For instance, in the Scott model of
PCF, the dcpos have carriers in the second universe $\mathcal{U}_1$ and suprema
of directed families with indexing type in the first universe $\mathcal{U}_0$.
Seeing a poset as a category in the usual way, we can say that these dcpos are
large, but locally small, and have small filtered colimits. In the case of
algebraic dcpos, in order to deal with size issues, we proceed mimicking the
definition of accessible category. With such a definition, our construction of
Scott's $D_\infty$ again gives a large, locally small, algebraic dcpo with
small directed suprema.
