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.

翻译：我们在一个Quillen模型范畴中构建了同伦类型理论的构造性模型，该模型在经典意义上呈现了通常空间的同伦理论。我们的模型基于笛卡尔立方范畴上的预层，这是一个表现良好的Eilenberg-Zilber范畴。关键创新在于立方Kan纤维化规范中增加了等变条件，这可以描述为立方集对称序列范畴中基于区间的一致纤维化类的拉回。我们模型开发过程中的主要技术结果已在计算机证明助手中形式化验证。