Division by Two, in Homotopy Type Theory

Authors Samuel Mimram , Émile Oleon

Thumbnail PDF


  • Filesize: 0.62 MB
  • 17 pages

Document Identifiers

Author Details

Samuel Mimram
  • École polytechnique, Palaiseau, France
Émile Oleon
  • École polytechnique, Palaiseau, France

Cite AsGet BibTex

Samuel Mimram and Émile Oleon. Division by Two, in Homotopy Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Natural numbers are isomorphism classes of finite sets and one can look for operations on sets which, after quotienting, allow recovering traditional arithmetic operations. Moreover, from a constructivist perspective, it is interesting to study whether those operations can be performed without resorting to the axiom of choice (the use of classical logic is usually necessary). Following the work of Bernstein, Sierpiński, Doyle and Conway, we study here "division by two" (or, rather, regularity of multiplication by two). We provide here a full formalization of this operation on sets, using the cubical variant of Agda, which is an implementation of the homotopy type theory setting, thus revealing some interesting points in the proof. As a novel contribution, we also show that this construction extends to general types, as opposed to sets.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • division
  • axiom of choice
  • set theory
  • homotopy type theory
  • Agda


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Felix Bernstein. Untersuchungen aus der Mengenlehre. Mathematische Annalen, 61(1):117-155, 1905. Google Scholar
  2. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. In 21st International Conference on Types for Proofs and Programs, number 69 in LIPIcs, page 262. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. URL: http://arxiv.org/abs/1611.02108.
  3. John Conway and Peter Doyle. Division by three, 1994. URL: http://arxiv.org/abs/math/0605779.
  4. Peter G Doyle and Cecil Qiu. Division by four, 2015. URL: http://arxiv.org/abs/1504.01402.
  5. Martín Hötzel Escardó. Introduction to univalent foundations of mathematics with Agda, 2019. URL: http://arxiv.org/abs/1911.00580.
  6. Martín Hötzel Escardó. The Cantor-Schröder-Bernstein Theorem for ∞-groupoids. Journal of Homotopy and Related Structures, 16(3):363-366, 2021. URL: http://arxiv.org/abs/2002.07079.
  7. Arie Hinkis. Proofs of the Cantor-Bernstein theorem. A mathematical excursion, volume 45 of Science Networks Historical Studies. Birkhäuser, 2013. Google Scholar
  8. Peter T Johnstone et al. Sketches of an Elephant: A Topos Theory Compendium: Volume 2, volume 2. Oxford University Press, 2002. Google Scholar
  9. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23(6):2071-2126, 2021. URL: http://arxiv.org/abs/1211.2851.
  10. Donnacha Oisín Kidney. A Small Proof that Fin is Injective. https://doisinkidney.com/posts/2019-11-15-small-proof-fin-inj.html, 2019.
  11. Adolf Lindenbaum and Alfred Tarski. Communication sur les recherches de le théorie des ensembles. 1926. Google Scholar
  12. Patrick Lutz. Conway Can Divide by Three, But I Can't, 2021. Google Scholar
  13. Samuel Mimram and Émile Oleon. Division by two in Agda, 2022. URL: https://github.com/smimram/div2.
  14. Pierre Pradic and Chad E Brown. Cantor-Bernstein implies Excluded Middle, 2019. URL: http://arxiv.org/abs/1904.09193.
  15. Rich Evan Schwartz. Pan galactic division. The Mathematical intelligencer, 37(3):8-10, 2015. URL: http://arxiv.org/abs/1504.02179.
  16. Wacław Sierpiński. Sur l'égalité 2m = 2n pour les nombres cardinaux. Fundamenta Mathematicae, 1(3):1-6, 1922. Google Scholar
  17. Andrew Swan. On Dividing by Two in Constructive Mathematics, 2018. URL: http://arxiv.org/abs/1804.04490.
  18. Alfred Tarski. Cancellation laws in the arithmetic of cardinals. Fundamenta Mathematicae, 36(1):77-92, 1949. Google Scholar
  19. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  20. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: a dependently typed programming language with univalence and higher inductive types. Journal of Functional Programming, 31, 2021. Google Scholar