Hypercubical manifolds in homotopy type theory

Abstract

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\'e 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.