de Jong, T., & Escardó, M. H. (2023). On Small Types in Univalent Foundations. Logical Methods in Computer Science, 19(2), 8:1-8:33. https://doi.org/10.46298/LMCS-19%282%3A8%292023