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
Univalent Types, Sets and Multisets: Investigations in dependent type theory
Stockholm University, Faculty of Science, Department of Mathematics. (Logic)
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. , p. 173
Keywords [en]
type theory, homotopy type theory, dependent types, constructive set theory, databases, formalisation, agda
National Category
Mathematics
Research subject
Mathematics
Identifiers
URN: urn:nbn:se:su:diva-136896ISBN: 978-91-7649-654-1 (print)ISBN: 978-91-7649-655-8 (print)OAI: oai:DiVA.org:su-136896DiVA, id: diva2:1057566
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
List of papers
1. Multisets in Type Theory
Open this publication in new window or tab >>Multisets in Type Theory
(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.

Keywords
multisets, type theory, homotopy type theory
National Category
Algebra and Logic
Research subject
Mathematics
Identifiers
urn:nbn:se:su:diva-136859 (URN)
Available from: 2016-12-16 Created: 2016-12-16 Last updated: 2016-12-22Bibliographically approved
2. From Multisets to Sets in Homotopy Type Theory
Open this publication in new window or tab >>From Multisets to Sets in Homotopy Type Theory
(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.

Keywords
constructive set theory, type theory, homotopy type theory
National Category
Mathematics
Research subject
Mathematics
Identifiers
urn:nbn:se:su:diva-136894 (URN)
Available from: 2016-12-19 Created: 2016-12-18 Last updated: 2016-12-22Bibliographically approved
3. Agda Formalisation
Open this publication in new window or tab >>Agda Formalisation
2016 (English)Other (Other academic)
Abstract [en]

The following is a formalisation of many of the proofs of arXiv:1610.08027 and arXiv:1612.05468 in Agda. Agda is a proof-checker and programming language based on dependent typetheory and pattern matching, which allow a very close correspondencebetween the style of proofs in the article and the formalised, machine-readable proof.

Publisher
p. 28
Keywords
agda, multisets, homotopy type theory
National Category
Mathematics
Research subject
Mathematical Logic
Identifiers
urn:nbn:se:su:diva-136903 (URN)
Available from: 2016-12-19 Created: 2016-12-19 Last updated: 2017-02-17Bibliographically approved
4. Type Theoretical Databases
Open this publication in new window or tab >>Type Theoretical Databases
(English)Manuscript (preprint) (Other academic)
Abstract [en]

We present a soundness theorem for a dependent type theory with context constants with respect to an indexed category of (finite, abstract) simplical complexes. The point of interest for computer science is that this category can be seen to represent tables in a natural way. Thus the category is a model for databases, a single mathematical structure in which all database schemas and instances (of a suitable, but sufficiently general form) are represented. The type theory then allows for the specification of database schemas and instances, the manipulation of the same with the usual type-theoretic operations, and the posing of queries.

Keywords
database, type theory, universe, schema, simplicial complex
National Category
Algebra and Logic Computer and Information Sciences
Research subject
Mathematics
Identifiers
urn:nbn:se:su:diva-136895 (URN)
Available from: 2016-12-18 Created: 2016-12-18 Last updated: 2018-01-13Bibliographically approved
5. Dependent Term Systems
Open this publication in new window or tab >>Dependent Term Systems
(English)Manuscript (preprint) (Other academic)
Abstract [en]

We consider two approaches to unravelling the dependency structures between terms independent type theory. The first approach defines a notion closely related to Cartmell'scategories with attributes, but with a separate operations for extending a context witha defined term. The second approach is closely related to Makkai's one-way categories —which form the signatures of his First-Order Logic with Dependent Sorts (FOLDS).This preliminary investigation provides the definitions and some basic results forboth approaches. We also formulate a few conjectures about how these two approaches relateto guide further investigation.

Keywords
dependent types, terms, one-way categories, categories with attributes
National Category
Mathematics
Research subject
Mathematical Logic
Identifiers
urn:nbn:se:su:diva-136899 (URN)
Available from: 2016-12-19 Created: 2016-12-19 Last updated: 2016-12-19

Open Access in DiVA

fulltext(2339 kB)151 downloads
File information
File name FULLTEXT02.pdfFile size 2339 kBChecksum SHA-512
33877a2685475fd34abd6b7a850067e988356b5bbe479110db80100749020113f3abe9a8b1f8a20f2a6dbb66d805bfabb89d1cdc6d50f8a2d987be09cdc380a0
Type fulltextMimetype application/pdf

Search in DiVA

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

Search outside of DiVA

GoogleGoogle Scholar
Total: 151 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 2082 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