Free Commutative Monoids in Homotopy Type Theory

conference
Authors
Affiliations

Vikraman Choudhury

Indiana University, USA / University of Cambridge, UK

Marcelo Fiore

University of Cambridge, UK

Published

February 22, 2023

Doi

10.46298/entics.10492

Abstract

We develop a constructive theory of finite multisets in Homotopy Type Theory, defining them as free commutative monoids. After recalling basic structural properties of the free commutative-monoid construction, we formalise and establish the categorical universal property of two, necessarily equivalent, algebraic presentations of free commutative monoids using 1-HITs. These presentations correspond to two different equational theories invariably including commutation axioms. In this setting, we prove important structural combinatorial properties of finite multisets. These properties are established in full generality without assuming decidable equality on the carrier set. As an application, we present a constructive formalisation of the relational model of classical linear logic and its differential structure. This leads to constructively establishing that free commutative monoids are conical refinement monoids. Thereon we obtain a characterisation of the equality type of finite multisets and a new presentation of the free commutative-monoid construction as a set-quotient of the list construction. These developments crucially rely on the commutation relation of creation/annihilation operators associated with the free commutative-monoid construction seen as a combinatorial Fock space.

Back to top

Citation

BibTeX citation:
@inproceedings{choudhury2023,
  author = {Choudhury, Vikraman and Fiore, Marcelo},
  title = {Free {Commutative} {Monoids} in {Homotopy} {Type} {Theory}},
  booktitle = {Electronic Notes in Theoretical Informatics and Computer
    Science},
  date = {2023},
  url = {https://doi.org/10.46298/entics.10492},
  doi = {10.46298/entics.10492},
  langid = {en},
  abstract = {We develop a constructive theory of finite multisets in
    Homotopy Type Theory, defining them as free commutative monoids.
    After recalling basic structural properties of the free
    commutative-monoid construction, we formalise and establish the
    categorical universal property of two, necessarily equivalent,
    algebraic presentations of free commutative monoids using 1-HITs.
    These presentations correspond to two different equational theories
    invariably including commutation axioms. In this setting, we prove
    important structural combinatorial properties of finite multisets.
    These properties are established in full generality without assuming
    decidable equality on the carrier set. As an application, we present
    a constructive formalisation of the relational model of classical
    linear logic and its differential structure. This leads to
    constructively establishing that free commutative monoids are
    conical refinement monoids. Thereon we obtain a characterisation of
    the equality type of finite multisets and a new presentation of the
    free commutative-monoid construction as a set-quotient of the list
    construction. These developments crucially rely on the commutation
    relation of creation/annihilation operators associated with the free
    commutative-monoid construction seen as a combinatorial Fock space.}
}
For attribution, please cite this work as:
Choudhury, Vikraman, and Marcelo Fiore. 2023. “Free Commutative Monoids in Homotopy Type Theory.” Electronic Notes in Theoretical Informatics and Computer Science, accepted. https://doi.org/10.46298/entics.10492.