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

, 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$

.