Examples and counterexamples of injective types

TL;DR

This paper explores various types in univalent mathematics, establishing which are injective, providing new examples, counterexamples, and linking injectivity to logical principles like the axiom of choice and weak excluded middle.

Contribution

It identifies new classes of injective types, analyzes their properties, and connects injectivity to foundational logical principles within univalent mathematics.

Findings

Type of ordinals, sets, and algebraic structures are injective.

Not all types are injective; some depend on logical principles.

Injectivity of certain types implies classical axioms like weak excluded middle.

Abstract

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 \v{S}\v{c}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.