标题： 对同伦类型的优雅模型的单值范畴 显示英文标题

标题： Univalent universes for elegant models of homotopy types

摘要： 我们在同伦类型的某些合适模型范畴中构造了Voevodsky意义上的统一宇宙（从Grothendieck的测试范畴理论中获得）。 实际上，这意味着除了单纯集的同伦理论之外，带有统一公理的内敛类型理论可以在立方集（带连接或不带连接）的同伦理论中进行解释，或者在Joyal的单元集的同伦理论中进行解释。 显示英文摘要

摘要： We construct a univalent universe in the sense of Voevodsky in some suitable model categories for homotopy types (obtained from Grothendieck's theory of test categories). In practice, this means for instance that, appart from the homotopy theory of simplicial sets, intensional type theory with the univalent axiom can be interpreted in the homotopy theory of cubical sets (with connections or not), or of Joyal's cellular sets.