License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2022.11
URN: urn:nbn:de:0030-drops-162920
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16292/
Go to the corresponding LIPIcs Volume Portal

Mimram, Samuel ; Oleon, Émile

Division by Two, in Homotopy Type Theory

pdf-format:
LIPIcs-FSCD-2022-11.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{mimram_et_al:LIPIcs.FSCD.2022.11,
  author =	{Mimram, Samuel and Oleon, \'{E}mile},
  title =	{{Division by Two, in Homotopy Type Theory}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16292},
  URN =		{urn:nbn:de:0030-drops-162920},
  doi =		{10.4230/LIPIcs.FSCD.2022.11},
  annote =	{Keywords: division, axiom of choice, set theory, homotopy type theory, Agda}
}

Keywords: division, axiom of choice, set theory, homotopy type theory, Agda
Collection: 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Issue Date: 2022
Date of publication: 28.06.2022
Supplementary Material: https://github.com/smimram/div2

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI