Hypercubical manifolds in homotopy type theory

Samuel Mimram, Émile Oleon

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 ho…