Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
From Multisets to Sets in Homotopy Type Theory
Stockholm University, Faculty of Science, Department of Mathematics.
(English)Manuscript (preprint) (Other academic)
Abstract [en]

We give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-L\"of type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel's 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of "Homotopy Type Theory" by the Univalent Foundations Program.

Keyword [en]
constructive set theory, type theory, homotopy type theory
National Category
Mathematics
Research subject
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-136894OAI: oai:DiVA.org:su-136894DiVA: diva2:1057523
Available from: 2016-12-19 Created: 2016-12-18 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:1612.05468

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar

Total: 446 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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