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

From Multisets to Sets in Homotopy 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();
}
}
(English)Manuscript (preprint) (Other academic)
##### Abstract [en]

##### Keywords [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, id: diva2:1057523
#####

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

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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt811",{id:"formSmash:j_idt811",widgetVar:"widget_formSmash_j_idt811",multiple:true}); Available from: 2016-12-19 Created: 2016-12-18 Last updated: 2016-12-22Bibliographically approved
##### In thesis

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.

1. Univalent Types, Sets and Multisets: Investigations in dependent type theory$(function(){PrimeFaces.cw("OverlayPanel","overlay1057566",{id:"formSmash:j_idt1257:0:j_idt1261",widgetVar:"overlay1057566",target:"formSmash:j_idt1257:0:parentLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

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

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