Hypercubical manifolds in homotopy type theory

Homotopy type theory is a logical setting in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces up to homotopy, and proofs as homotopy invariant constructions. In this context, we introduce a type which corresponds to the hypercubical manifold, a space first introduced by Poincaré in 1895. Its importance stems from the fact that it provides an approximation of the group Q of quaternionic units, in the sense of being the first step of a cellular resolution of Q. In order to ensure the validity of our definition, we show that it satisfies the expected property: it is the homotopy quotient of the 3-sphere by the expected action of Q. This is non-trivial and requires performing subtle combinatorial computations based on the flattening lemma, thus illustrating the effective nature of homotopy type theory. Finally, based on the previous construction, we introduce new higher-dimensional generalizations of this manifold, which correspond to better cellular approximations of Q, converging toward a delooping of Q.