DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2024.6

Delooping Generated Groups in Homotopy Type Theory

Authors: Camil Champin, Samuel Mimram, and Émile Oleon

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract

Homotopy type theory is a logical setting based on Martin-Löf type theory in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces (up to continuous deformation) and proofs as homotopy invariant constructions. In this context, loop spaces of pointed connected groupoids provide a natural representation of groups, and any group can be obtained as the loop space of such a type, which is then called a delooping of the group. There are two main methods to construct the delooping of an arbitrary group G. The first one consists in describing it as a pointed higher inductive type, whereas the second one consists in taking the connected component of the principal G-torsor in the type of sets equipped with an action of G. We show here that, when a presentation is known for the group, simpler variants of those constructions can be used to build deloopings. The resulting types are more amenable to computations and lead to simpler meta-theoretic reasoning. We also investigate, in this context, an abstract construction for the Cayley graph of a generated group and show that it encodes the relations of the group. Most of the developments performed in the article have been formalized using the cubical version of the Agda proof assistant.

Cite as

Camil Champin, Samuel Mimram, and Émile Oleon. Delooping Generated Groups in Homotopy Type Theory. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{champin_et_al:LIPIcs.FSCD.2024.6,
  author =	{Champin, Camil and Mimram, Samuel and Oleon, \'{E}mile},
  title =	{{Delooping Generated Groups in Homotopy Type Theory}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{6:1--6:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.6},
  URN =		{urn:nbn:de:0030-drops-203356},
  doi =		{10.4230/LIPIcs.FSCD.2024.6},
  annote =	{Keywords: homotopy type theory, delooping, group, generator, Cayley graph}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2022.11

Division by Two, in Homotopy Type Theory

Authors: Samuel Mimram and Émile Oleon

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

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.

Cite as

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.FSCD.2022.11},
  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}
}

Search Results

Documents authored by Oleon, Émile

Delooping Generated Groups in Homotopy Type Theory

Abstract

Cite as

Division by Two, in Homotopy Type Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message