Subtype Universes. - Harry Maclean; Zhaohui Luo (TYPES, 2020)