On Commutativity, Total Orders, and Sorting

workshop
Authors
Affiliations

Wind Wong

University of Glasgow, Glasgow, UK

Vikraman Choudhury

Università di Bologna, Bologna, Italy

Simon J Gay

University of Glasgow, Glasgow, UK

Published

April 1, 2024

Abstract

In this talk, we study free monoids, free commutative monoids, and their connections with sorting and well-orders. Univalent type theory provides a rigorous framework for implementing these ideas, in the construction of free algebras using higher inductive types and quotients, and reasoning up to equivalence using categorical universal properties. The main contributions are a new framework for universal algebra (free algebras and their universal properties), various constructions of free monoids and free commutative monoids (with proofs of their universal properties), applications to proving combinatorial properties of these constructions, and finally an axiomatic understanding of sorting. Our results have been formalized in Cubical Agda, and the formalization is available at: https://github.com/pufferffish/agda-symmetries/.

Back to top

Citation

BibTeX citation:
@inproceedings{wong2024,
  author = {Wong, Wind and Choudhury, Vikraman and J Gay, Simon},
  title = {On {Commutativity,} {Total} {Orders,} and {Sorting}},
  booktitle = {Workshop on Homotopy Type Theory / Univalent Foundations
    (HoTT/UF 2024)},
  date = {2024},
  url = {https://vikraman.org/papers/wong-choudhury-gay-2024/},
  langid = {en},
  abstract = {In this talk, we study free monoids, free commutative
    monoids, and their connections with sorting and well-orders.
    Univalent type theory provides a rigorous framework for implementing
    these ideas, in the construction of free algebras using higher
    inductive types and quotients, and reasoning up to equivalence using
    categorical universal properties. The main contributions are a new
    framework for universal algebra (free algebras and their universal
    properties), various constructions of free monoids and free
    commutative monoids (with proofs of their universal properties),
    applications to proving combinatorial properties of these
    constructions, and finally an axiomatic understanding of sorting.
    Our results have been formalized in Cubical Agda, and the
    formalization is available at:
    https://github.com/pufferffish/agda-symmetries/.}
}
For attribution, please cite this work as:
Wong, Wind, Vikraman Choudhury, and Simon J Gay. 2024. “On Commutativity, Total Orders, and Sorting.” Workshop on Homotopy Type Theory / Univalent Foundations (HoTT/UF 2024), accepted. https://vikraman.org/papers/wong-choudhury-gay-2024/.