一句话：在同伦类型论中用高阶归纳类型与 tautological bundle 归纳构造实射影空间。
论文研究如何在同伦类型论中构造实射影空间。经典定义将 ℝP^n 视为 n 维球面认同对径点所得的商空间，但该定义无法直接翻译到同伦类型论。作者改为对 n 归纳地定义 ℝP^n，并同时定义其由二元集合构成的 tautological bundle：基例取 ℝP^{-1} 为空类型；归纳步将 ℝP^{n+1} 定义为 ℝP^n 的 tautological bundle 投影映射的 mapping cone，并借助万有性质与 univalence 公理定义 ℝP^{n+1} 上的 tautological bundle。该工作表明实射影空间可作为高阶归纳类型在同伦类型论内部构造，为在同伦类型论中开展同伦论提供了基础。
Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of ℝP<sup>n</sup>, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define ℝP<sup>n</sup> by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take ℝP<sup>−1</sup> to be the empty type. In the inductive step, we take ℝP<sup>n+1</sup> to be the mapping cone of the projection map of the tautological bundle of ℝP<sup>n</sup>, and we use its universal property and the univalence axiom to define the tautological bundle on ℝP<sup>n+1</sup>.