标题： 关于笛卡尔立方集合的等变模型结构 显示英文标题

标题： The equivariant model structure on cartesian cubical sets

摘要： 我们发展了一个构造性的同伦类型论模型在一个Quillen模型范畴中，经典地给出了通常的空间同伦理论。我们的模型基于笛卡尔立方范畴上的预层，这是一个具有良好行为的艾伦伯格-齐尔伯范畴。关键的创新是在立方体Kan纤维化的规范中增加了一个等变条件，这可以被描述为基于区间的一类均匀纤维在立方体集合对称序列范畴中的拉回。我们在模型发展中得到的主要技术结果已经在计算机证明助手里形式化了。 显示英文摘要

摘要： We develop a constructive model of homotopy type theory in a Quillen model category that classically presents the usual homotopy theory of spaces. Our model is based on presheaves over the cartesian cube category, a well-behaved Eilenberg-Zilber category. The key innovation is an additional equivariance condition in the specification of the cubical Kan fibrations, which can be described as the pullback of an interval-based class of uniform fibrations in the category of symmetric sequences of cubical sets. The main technical results in the development of our model have been formalized in a computer proof assistant.