LIPIcs.FSCD.2022.11.pdf
- Filesize: 0.62 MB
- 17 pages
Document
Division by Two, in Homotopy Type Theory
Authors
Samuel Mimram 
,
-
Part of:
Volume:
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Formal Structures for Computation and Deduction (FSCD) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-28
File
Document Identifiers
Author Details
Cite As Get 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)
https://doi.org/10.4230/LIPIcs.FSCD.2022.11
Abstract
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
Keywords
- division
- axiom of choice
- set theory
- homotopy type theory
- Agda
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Felix Bernstein. Untersuchungen aus der Mengenlehre. Mathematische Annalen, 61(1):117-155, 1905.
- 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.
- John Conway and Peter Doyle. Division by three, 1994. URL: http://arxiv.org/abs/math/0605779.
- Peter G Doyle and Cecil Qiu. Division by four, 2015. URL: http://arxiv.org/abs/1504.01402.
- Martín Hötzel Escardó. Introduction to univalent foundations of mathematics with Agda, 2019. URL: http://arxiv.org/abs/1911.00580.
- 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.
-
Arie Hinkis. Proofs of the Cantor-Bernstein theorem. A mathematical excursion, volume 45 of Science Networks Historical Studies. Birkhäuser, 2013.
-
Peter T Johnstone et al. Sketches of an Elephant: A Topos Theory Compendium: Volume 2, volume 2. Oxford University Press, 2002.
- 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.
- Donnacha Oisín Kidney. A Small Proof that Fin is Injective. https://doisinkidney.com/posts/2019-11-15-small-proof-fin-inj.html, 2019.
-
Adolf Lindenbaum and Alfred Tarski. Communication sur les recherches de le théorie des ensembles. 1926.
-
Patrick Lutz. Conway Can Divide by Three, But I Can't, 2021.
- Samuel Mimram and Émile Oleon. Division by two in Agda, 2022. URL: https://github.com/smimram/div2.
- Pierre Pradic and Chad E Brown. Cantor-Bernstein implies Excluded Middle, 2019. URL: http://arxiv.org/abs/1904.09193.
- Rich Evan Schwartz. Pan galactic division. The Mathematical intelligencer, 37(3):8-10, 2015. URL: http://arxiv.org/abs/1504.02179.
-
Wacław Sierpiński. Sur l'égalité 2m = 2n pour les nombres cardinaux. Fundamenta Mathematicae, 1(3):1-6, 1922.
- Andrew Swan. On Dividing by Two in Constructive Mathematics, 2018. URL: http://arxiv.org/abs/1804.04490.
-
Alfred Tarski. Cancellation laws in the arithmetic of cardinals. Fundamenta Mathematicae, 36(1):77-92, 1949.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
-
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.