Hypercubical manifolds in homotopy type theory

TL;DR

This paper introduces hypercubical manifolds within homotopy type theory, providing new geometric constructions that approximate quaternionic groups and generalize to higher dimensions, demonstrating the theory's computational effectiveness.

Contribution

It defines hypercubical manifolds in homotopy type theory and constructs higher-dimensional generalizations that better approximate quaternionic groups.

Findings

Successfully models hypercubical manifolds as homotopy quotients of spheres.

Performs combinatorial computations validating the manifold definitions.

Introduces higher-dimensional generalizations approaching a delooping of Q.

Abstract

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