A fresh look at commutativity: free algebraic structures via fresh lists

Research output: Contribution to conferencePaperpeer-review

15 Downloads (Pure)

Abstract

We show how types of finite sets and multisets can be constructed in ordinary dependent type theory, without the need for quotient types or working with setoids, and prove that these constructions realise finite sets and multisets as free idempotent commutative monoids and free commutative monoids, respectively. Both constructions arise as generalisations of C. Coquand’s data type of fresh lists, and we show how many other free structures also can be realised by other instantiations. All of our results have been formalised in Agda.
Original languageEnglish
Pages1-20
Number of pages20
Publication statusE-pub ahead of print - 29 Nov 2023
EventThe 21st Asian Symposium on Programming Languages and Systems - Taipei, Taiwan
Duration: 26 Nov 202329 Nov 2023
Conference number: 21
https://conf.researchr.org/home/aplas-2023

Conference

ConferenceThe 21st Asian Symposium on Programming Languages and Systems
Abbreviated titleAPLAS
Country/TerritoryTaiwan
CityTaipei
Period26/11/2329/11/23
Internet address

Keywords

  • free algebraic structures
  • fresh lists
  • dependent type theory

Fingerprint

Dive into the research topics of 'A fresh look at commutativity: free algebraic structures via fresh lists'. Together they form a unique fingerprint.

Cite this