  We investigate the injective types and the algebraically injective types in
univalent mathematics, both in the absence and in the presence of propositional
resizing. Injectivity is defined by the surjectivity of the restriction map
along any embedding, and algebraic injectivity is defined by a given section of
the restriction map along any embedding. Under propositional resizing axioms,
the main results are easy to state: (1) Injectivity is equivalent to the
propositional truncation of algebraic injectivity. (2) The algebraically
injective types are precisely the retracts of exponential powers of universes.
(2a) The algebraically injective sets are precisely the retracts of powersets.
(2b) The algebraically injective $(n+1)$-types are precisely the retracts of
exponential powers of universes of $n$-types. (3) The algebraically injective
types are also precisely the retracts of algebras of the partial-map
classifier. From (2) it follows that any universe is embedded as a retract of
any larger universe. In the absence of propositional resizing, we have similar
results which have subtler statements that need to keep track of universe
levels rather explicitly, and are applied to get the results that require
resizing.
