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é in 1895. This manifold is interesting because it offers an approximation of the quaternion group upper Q Q $Q$ , in the sense that it represents the first step toward the construction of a cellular resolution of upper Q Q $Q$ . To validate our definition, we show that it satisfies the expected property: it is the homotopy quotient of the 3-sphere normal upper S cubed S 3 $\operatorname {S}^{3}$ under the natural action of upper Q Q $Q$ . Establishing this result is nontrivial, 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 upper Q Q $Q$ and converge toward a delooping of upper Q Q $Q$ .