Univalent Types, Sets and Multisets : Investigations in dependent type theory
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 way...
Main Author: | Robbestad Gylterud, Håkon |
---|---|
Format: | Doctoral Thesis |
Language: | English |
Published: |
Stockholms universitet, Matematiska institutionen
2017
|
Subjects: | |
Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-136896 http://nbn-resolving.de/urn:isbn:978-91-7649-654-1 http://nbn-resolving.de/urn:isbn:978-91-7649-655-8 |
Similar Items
-
Programming Metamorphic Algorithms: An Experiment in Type-Driven Algorithm Design
by: Ko, H.-S
Published: (2021) -
Sur les groupes d’homotopie des sphères en théorie des types homotopiques
by: Brunerie, Guillaume
Published: (2016) -
Lawvere-Tierney sheafification in Homotopy Type Theory
by: Quirin, Kevin
Published: (2016) -
Lawvere-Tierney sheafification in Homotopy Type Theory
by: Kevin Quirin, et al.
Published: (2016-12-01) -
Modèles de l'univalence dans le cadre équivariant
by: Bordg, Anthony
Published: (2015)