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 $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 $\operatorname {S}^{3}$ under the natural action of $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 $Q$ and converge toward a delooping of $Q$.

Weak $\omega$-categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of weak $\omega$-groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this definition of globular weak $\omega$-groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type theory called $\mathsf{CaTT}$, whose models are weak $\omega$-categories. Here, we generalize this approach to monoidal weak $\omega$-categories. Based on the principle that they should be equivalent to weak $\omega$-categories with only one 0-cell, we are able to derive a type theory $\mathsf{MCaTT}$ whose models are monoidal weak $\omega$-categories. This requires changing the rules of the theory in order to encode the information carried by the unique 0-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory $\mathsf{MCaTT}$ and the type theory $\mathsf{CaTT}$. Our main contribution is to show that these translations relate the models of our type theory to the models of the type theory $\mathsf{CaTT}$ consisting of $\omega$-categories with only one 0-cell by analyzing in details how the notion of models interact with the structural rules of both type theories.