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 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 under the natural action of Q. Establishing this result is non-trivial, 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.
From: Samuel Mimram [view email]
[v1]
Tue, 24 Jun 2025 08:12:29 UTC (27 KB)
[v2]
Fri, 12 Jun 2026 07:21:42 UTC (31 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。