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

Exact completion and type-theoretic structuresPrimeFaces.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();
}
}
2019 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

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

Stockholm: Department of Mathematics, Stockholm University , 2019. , p. 23
##### Keywords [en]

exact completion, type theory, setoid, weak limits, cartesian closure, inductive types
##### National Category

Algebra and Logic
##### Research subject

Mathematics
##### Identifiers

URN: urn:nbn:se:su:diva-162275ISBN: 978-91-7797-526-7 (print)ISBN: 978-91-7797-527-4 (electronic)OAI: oai:DiVA.org:su-162275DiVA, id: diva2:1264924
##### Public defence

2019-01-18, sal 14, hus 5, Kräftriket, Roslagsvägen 101, Stockholm, 13:00 (English)
##### Opponent

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

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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt559",{id:"formSmash:j_idt559",widgetVar:"widget_formSmash_j_idt559",multiple:true});
##### Note

##### List of papers

This thesis consists of four papers and is a contribution to the study of representations of extensional properties in intensional type theories using, mainly, the language and tools from category theory. Our main focus is on exact completions of categories with weak finite limits as a category-theoretic description of the setoid construction in Martin-Löf's intensional type theory.

Paper I, which is joint work with Erik Palmgren, provides sufficient conditions for such an exact completion to produce a model of the system CETCS (Constructive Elementary Theory of the Category of Sets), a finite axiomatisation of the theory of well-pointed locally cartesian closed pretoposes with a natural numbers object and enough projectives. In particular, we use a condition inspired by Aczel's set-theoretic Fullness Axiom to obtain the local cartesian closure of an exact completion. As an application, we obtain a simple uniform proof that the category of setoids is a model of CETCS.

Paper II was prompted by the discovery of an overlooked issue in the characterisationof local cartesian closure for exact completions due to Carboni and Rosolini. In this paper we clarify the problem, show that their characterisation is still valid when the base category has finite limits, and provide a complete solution in the general case of a category with weak finite limits.

In paper III we generalise the approach used in paper I to obtain the local cartesian closure of an exact completion to arbitrary categories with finite limits. We then show how this condition inspired by the Fullness Axiom naturally arises in several homotopy categories and apply this result to obtain the local cartesian closure of the exact completion of the homotopy category of spaces, thus answering a question left open by Marino Gran and Enrico Vitale.

Finally, in paper IV we abandon the pure category-theoretic approach and instead present a type-theoretic construction, formalised in Coq, of W-types in the category of setoids from dependent W-types in the underlying intensional theory. In particular, contrary to previous approaches, this construction does not require the assumption of Uniqueness of Identity Proofs nor recursion into a type universe.

At the time of the doctoral defense, the following papers were unpublished and had a status as follows: Paper 1: Manuscript. Paper 2: Manuscript. Paper 3: Manuscript. Paper 4: Manuscript.

Available from: 2018-12-19 Created: 2018-11-21 Last updated: 2018-12-07Bibliographically approved1. Exact completion and constructive theories of sets$(function(){PrimeFaces.cw("OverlayPanel","overlay1176023",{id:"formSmash:j_idt613:0:j_idt617",widgetVar:"overlay1176023",target:"formSmash:j_idt613:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. On the local cartesian closure of exact completions$(function(){PrimeFaces.cw("OverlayPanel","overlay1242506",{id:"formSmash:j_idt613:1:j_idt617",widgetVar:"overlay1242506",target:"formSmash:j_idt613:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

3. The Fullness Axiom and exact completions of homotopy categories$(function(){PrimeFaces.cw("OverlayPanel","overlay1264883",{id:"formSmash:j_idt613:2:j_idt617",widgetVar:"overlay1264883",target:"formSmash:j_idt613:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

4. W-types in setoids$(function(){PrimeFaces.cw("OverlayPanel","overlay1264884",{id:"formSmash:j_idt613:3:j_idt617",widgetVar:"overlay1264884",target:"formSmash:j_idt613:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

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

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