2026-07-24T21:21:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16292 2024-03-06T10:57:09Z ddc:004 open_access

Division by Two, in Homotopy Type Theory Mimram, Samuel Oleon, Émile division axiom of choice set theory homotopy type theory Agda 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Samuel Mimram and Émile Oleon 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.11 urn:nbn:de:0030-drops-162920 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.11 eng https://creativecommons.org/licenses/by/4.0/legalcode