Examples and counterexamples of injective types

Tom de Jong, Martín Hötzel Escardó

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 mona…