de Jong, Tom, Escardó, Martín Hötzel, "On Small Types in Univalent Foundations", Logical Methods in Computer Science, 2023