TY - GEN
T1 - Division by Two, in Homotopy Type Theory
AU - Mimram, Samuel
AU - Oleon, Émile
N1 - Publisher Copyright:
© Samuel Mimram and Émile Oleon
PY - 2022/6/1
Y1 - 2022/6/1
N2 - 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.
AB - 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.
KW - Agda
KW - axiom of choice
KW - division
KW - homotopy type theory
KW - set theory
U2 - 10.4230/LIPIcs.FSCD.2022.11
DO - 10.4230/LIPIcs.FSCD.2022.11
M3 - Conference contribution
AN - SCOPUS:85133713390
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
A2 - Felty, Amy P.
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
Y2 - 2 August 2022 through 5 August 2022
ER -