We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Free Commutative Monoids in Homotopy Type Theory

Abstract: We develop a constructive theory of finite multisets, defining them as free commutative monoids in Homotopy Type Theory.
We formalise two algebraic presentations of this construction using 1-HITs, establishing the universal property for each and thereby their equivalence. These presentations correspond to equational theories including a commutation axiom.
In this setting, we prove important structural combinatorial properties of singleton multisets arising from concatenations and projections of multisets. This is done in generality, without assuming decidable equality on the carrier set.
Further, as applications, we present a constructive formalisation of the relational model of differential linear logic and use it to characterise the equality type of multisets.
This leads us to the introduction of a novel conditional equational presentation of the finite-multiset construction.
Comments: Under submission
Subjects: Logic in Computer Science (cs.LO); Combinatorics (math.CO); Category Theory (math.CT); Logic (math.LO)
MSC classes: 03G30
ACM classes: F.4.1
Cite as: arXiv:2110.05412 [cs.LO]
  (or arXiv:2110.05412v1 [cs.LO] for this version)

Submission history

From: Vikraman Choudhury [view email]
[v1] Mon, 11 Oct 2021 16:59:16 GMT (70kb)

Link back to: arXiv, form interface, contact.