Homotopy type theory provides a logical framework in which geometric constructions and proofs can be carried out synthetically: in this setting, types correspond to spaces up to homotopy, and proofs to homotopy-invariant constructions. Within this context, we introduce a type corresponding to the hypercubical manifold, a space first described by Poincaré in 1895. This manifold is interesting because it offers an approximation of the quaternion group Q, in the sense that it represents the first step toward the construction of a cellular resolution of Q. To validate our definition, we show that it satisfies the expected property: it is the homotopy quotient of the 3-sphere under the natural action of Q. Establishing this result is non-trivial, requiring subtle combinatorial computations based on the flattening lemma, thereby illustrating the constructive power of homotopy type theory. Finally, extending this construction, we introduce higher-dimensional generalizations of the manifold, which provide increasingly precise cellular approximations of Q, and converge toward a delooping of Q.

翻译：同伦类型论提供了一个逻辑框架，在其中可以综合地进行几何构造与证明：在该框架中，类型对应于同伦意义下的空间，而证明则对应于同伦不变的构造。在此背景下，我们引入了一种对应于超立方流形的类型——该空间最早由庞加莱于1895年描述。这一流形之所以引人关注，是因为它在四元数群Q的胞腔分解构造中代表了第一步，从而提供了Q的一种近似。为验证这一定义，我们证明其满足预期性质：它是在Q的自然作用下三维球面的同伦商。建立这一结果并非易事，需要基于展平引理进行精妙的组合计算，从而展示了同伦类型论的构造能力。最后，通过扩展这一构造，我们引入了该流形的高维推广，这些推广提供了Q的越来越精确的胞腔近似，并收敛于Q的一个去环路化。