Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Multisets in Type Theory
Stockholm University, Faculty of Science, Department of Mathematics.
(English)Manuscript (preprint) (Other academic)
Abstract [en]

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öf 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.

Keyword [en]
multisets, type theory, homotopy type theory
National Category
Algebra and Logic
Research subject
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-136859OAI: oai:DiVA.org:su-136859DiVA: diva2:1057274
Available from: 2016-12-16 Created: 2016-12-16 Last updated: 2016-12-22Bibliographically approved
In thesis
1. Univalent Types, Sets and Multisets: Investigations in dependent type theory
Open this publication in new window or tab >>Univalent Types, Sets and Multisets: Investigations in dependent type theory
2017 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

This thesis consists of four papers on type theory and a formalisation of certain results from the two first papers in the Agda language. We cover topics such as models of multisets and sets in Homotopy Type Theory, and explore ideas of using type theory as a language for databases and different ways of expressing dependencies between terms. The two first papers build on work by Aczel 1978. We establish that the underlying type of Aczel’s model of set theory in type theory can be seen as a type of multisets from the perspective of Homotopy Type Theory, and we identify a suitable subtype which becomes a model of set theory in which equality of sets is the identity type. The third paper is joint work with Henrik Forssell and David I .Spivak and explores a certain model of type theory, consisting of simplicial complexes, from the perspective of database theory. In the fourth and final paper, we consider two approaches to unraveling the dependency structures between terms in dependent type theory, and formulate a few conjectures about how these two approaches relate.

Place, publisher, year, edition, pages
Stockholm: Department of Mathematics, Stockholm University, 2017. 173 p.
Keyword
type theory, homotopy type theory, dependent types, constructive set theory, databases, formalisation, agda
National Category
Mathematics
Research subject
Mathematics
Identifiers
urn:nbn:se:su:diva-136896 (URN)978-91-7649-654-1 (ISBN)978-91-7649-655-8 (ISBN)
Public defence
2017-02-09, sal 14, hus 5, Kräftriket, Roslagsvägen 101, Stockholm, 13:00 (English)
Opponent
Supervisors
Available from: 2017-01-17 Created: 2016-12-18 Last updated: 2017-01-17Bibliographically approved

Open Access in DiVA

No full text

Other links

arXiv:1610.08027

Search in DiVA

By author/editor
Robbestad Gylterud, Håkon
By organisation
Department of Mathematics
Algebra and Logic

Search outside of DiVA

GoogleGoogle Scholar

Total: 27 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf