Vikraman Choudhury ; Marcelo Fiore - Free Commutative Monoids in Homotopy Type Theory

entics:10492 - Electronic Notes in Theoretical Informatics and Computer Science, February 22, 2023, Volume 1 - Proceedings of MFPS XXXVIII -
Free Commutative Monoids in Homotopy Type TheoryArticle

Authors: Vikraman Choudhury ; Marcelo Fiore

    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.

    Volume: Volume 1 - Proceedings of MFPS XXXVIII
    Published on: February 22, 2023
    Accepted on: January 19, 2023
    Submitted on: December 16, 2022
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Combinatorics,Mathematics - Category Theory,Mathematics - Logic,03G30,F.4.1

    1 Document citing this article

    Consultation statistics

    This page has been seen 334 times.
    This article's PDF has been downloaded 234 times.