Injective types in univalentmathematics

摘要

We investigate the injective types and the algebraically injective types in univalent mathematics, both inthe absence and in the presence of propositional resizing. Injectivity is defined by the surjectivity of therestriction map along any embedding, and algebraic injectivity is defined by a given section of the restrictionmap 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 algebraicallyinjective types are precisely the retracts of exponential powers of universes. (2a) The algebraically injectivesets are precisely the retracts of powersets. (2b) The algebraically injective (n+1)-types are precisely theretracts of exponential powers of universes of n-types. (3) The algebraically injective types are also preciselythe retracts of algebras of the partial-map classifier. From (2) it follows that any universe is embedded asa retract of any larger universe. In the absence of propositional resizing, we have similar results that havesubtler statements which need to keep track of universe levels rather explicitly, and are applied to get theresults that require resizing.