It is known that, in univalent mathematics, type universes, the type of $n$-types in a universe, reflective subuniverses, and the underlying type of any algebra of the lifting monad are all (algebraically) injective. Here, we further show that the type of ordinals, the type of iterative (multi)sets, the underlying type of any pointed directed complete poset, as well as the types of (small) $\infty$-magmas, monoids, and groups are all injective, among other examples. Not all types of mathematical structures are injective in general. For example, the type of inhabited types is injective if and only if all propositions are projective. In contrast, the type of pointed types and the type of non-empty types are always injective. The injectivity of the type of two-element types implies Fourman and Ščedrov's world's simplest axiom of choice. We also show that there are no nontrivial small injective types unless a weak propositional resizing principle holds. Other counterexamples include the type of booleans, the simple types, the type of Dedekind reals, and the type of conatural numbers, whose injectivity implies weak excluded middle. More generally, any type with an apartness relation and two points apart cannot be injective unless weak excluded middle holds. Finally, we show that injective types have no non-trivial decidable properties, unless weak excluded middle holds, which amounts to a Rice-like theorem for injective types.

翻译：已知在单值数学中，类型宇宙、宇宙中n-类型构成的类型、反射子宇宙，以及提升单子任意代数的底层类型都是（代数）内射的。本文进一步证明：序数类型、迭代（多）集合类型、任意带点有向完备偏序集的底层类型，以及（小）∞-幺半群、幺半群和群的类型均为内射类型，此外还包括其他示例。并非所有数学结构的类型都具有普遍内射性。例如，非空类型的类型是内射的当且仅当所有命题都是投射的。相比之下，带点类型的类型与非空类型的类型总是内射的。二元类型的内射性蕴含Fourman与Ščedrov提出的"世界最简单选择公理"。我们还证明：除非弱命题重置原理成立，否则不存在非平凡的小内射类型。其他反例包括布尔值类型、简单类型、戴德金实数类型以及余自然数类型——这些类型的内射性将蕴含弱排中律。更一般地，任何具有不等关系且包含两个相异元素的类型都不是内射的，除非弱排中律成立。最后我们证明：除非弱排中律成立，否则内射类型不具有非平凡的可判定性质，这相当于针对内射类型的Rice型定理。