Multisets in type theory

DOI10.1017/S0305004119000045MaRDI QIDQ4958648zbMATH OpenOpenAlexWikidataFDO

Authors Håkon Robbestad Gylterud

Publication date 14 September 2021

Published in Mathematical Proceedings of the Cambridge Philosophical Society (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1610.08027

Mathematics Subject Classification ID

Type theory (03B38) Metamathematics of constructive systems (03F50)

Abstract: A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin-L"of Type Theory, in the presence of Voevodsky's Univalence Axiom. Aczel 1978 introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the Univalence Axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.

Recommendations

• From multisets to sets in homotopy type theory
• Multiset theory
• A single-sorted theory of multisets
• Multisets, heaps, bags, families: what is a multiset?
• Mathematics of multisets in the Fraenkel-Mostowski framework

Cites work

• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• Multiset theory
• The cardinal module and some theorems on families of sets
• Voevodsky’s Univalence Axiom in Homotopy Type Theory

Cited in

(12)

• Multisets and structural congruence of the pi-calculus with replication
• scientific article; zbMATH DE number 5081042 (Why is no real title available?)
• From multisets to sets in homotopy type theory
• Sets, types and type-checking
• scientific article; zbMATH DE number 7204430 (Why is no real title available?)
• W-types in setoids
• Type inference for set theory
• Free commutative monoids in homotopy type theory
• Univalent material set theory
• The category of iterative sets in homotopy type theory and univalent foundations
• Terminal coalgebras and non-wellfounded sets in homotopy type theory
• A single-sorted theory of multisets

This page was built for publication: Multisets in type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4958648)