CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt144",{id:"formSmash:upper:j_idt144",widgetVar:"widget_formSmash_upper_j_idt144",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt145_j_idt147",{id:"formSmash:upper:j_idt145:j_idt147",widgetVar:"widget_formSmash_upper_j_idt145_j_idt147",target:"formSmash:upper:j_idt145:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Univalent Types, Sets and Multisets: Investigations in dependent type theoryPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
PrimeFaces.cw("AccordionPanel","widget_formSmash_responsibleOrgs",{id:"formSmash:responsibleOrgs",widgetVar:"widget_formSmash_responsibleOrgs",multiple:true}); 2017 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Stockholm: Department of Mathematics, Stockholm University , 2017. , p. 173
##### Keyword [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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt432",{id:"formSmash:j_idt432",widgetVar:"widget_formSmash_j_idt432",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt438",{id:"formSmash:j_idt438",widgetVar:"widget_formSmash_j_idt438",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt444",{id:"formSmash:j_idt444",widgetVar:"widget_formSmash_j_idt444",multiple:true});
Available from: 2017-01-17 Created: 2016-12-18 Last updated: 2017-01-17Bibliographically approved
##### List of papers

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.

1. Multisets in Type Theory$(function(){PrimeFaces.cw("OverlayPanel","overlay1057274",{id:"formSmash:j_idt480:0:j_idt484",widgetVar:"overlay1057274",target:"formSmash:j_idt480:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. From Multisets to Sets in Homotopy Type Theory$(function(){PrimeFaces.cw("OverlayPanel","overlay1057523",{id:"formSmash:j_idt480:1:j_idt484",widgetVar:"overlay1057523",target:"formSmash:j_idt480:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

3. Agda Formalisation$(function(){PrimeFaces.cw("OverlayPanel","overlay1057544",{id:"formSmash:j_idt480:2:j_idt484",widgetVar:"overlay1057544",target:"formSmash:j_idt480:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

4. Type Theoretical Databases$(function(){PrimeFaces.cw("OverlayPanel","overlay1057510",{id:"formSmash:j_idt480:3:j_idt484",widgetVar:"overlay1057510",target:"formSmash:j_idt480:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

5. Dependent Term Systems$(function(){PrimeFaces.cw("OverlayPanel","overlay1057524",{id:"formSmash:j_idt480:4:j_idt484",widgetVar:"overlay1057524",target:"formSmash:j_idt480:4:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

isbn
urn-nbn$(function(){PrimeFaces.cw("Tooltip","widget_formSmash_j_idt1141",{id:"formSmash:j_idt1141",widgetVar:"widget_formSmash_j_idt1141",showEffect:"fade",hideEffect:"fade",showDelay:500,hideDelay:300,target:"formSmash:altmetricDiv"});});

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1194",{id:"formSmash:lower:j_idt1194",widgetVar:"widget_formSmash_lower_j_idt1194",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1195_j_idt1197",{id:"formSmash:lower:j_idt1195:j_idt1197",widgetVar:"widget_formSmash_lower_j_idt1195_j_idt1197",target:"formSmash:lower:j_idt1195:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});