References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt145",{id:"formSmash:upper:j_idt145",widgetVar:"widget_formSmash_upper_j_idt145",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt146_j_idt148",{id:"formSmash:upper:j_idt146:j_idt148",widgetVar:"widget_formSmash_upper_j_idt146_j_idt148",target:"formSmash:upper:j_idt146:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

On Constructive Sets and Partial 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();
}
}
PrimeFaces.cw("AccordionPanel","widget_formSmash_responsibleOrgs",{id:"formSmash:responsibleOrgs",widgetVar:"widget_formSmash_responsibleOrgs",multiple:true}); 2011 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

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

Uppsala: Department of Mathematics , 2011. , 33 p.
##### Series

Uppsala Dissertations in Mathematics, ISSN 1401-2049 ; 74
##### National Category

Algebra and Logic
##### Research subject

Mathematical Logic
##### Identifiers

URN: urn:nbn:se:uu:diva-160605ISBN: 978-91-506-2245-4OAI: oai:DiVA.org:uu-160605DiVA: diva2:451872
##### Public defence

2011-12-13, Polhemsalen, Ångströmlaboratoriet, Lägerhyddsvägen 1, Uppsala, 13:15 (English)
##### Opponent

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

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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt387",{id:"formSmash:j_idt387",widgetVar:"widget_formSmash_j_idt387",multiple:true});
Available from: 2011-11-22 Created: 2011-10-27 Last updated: 2011-12-15Bibliographically approved
##### List of papers

The first three papers in this thesis study the formalisation of a set in type theory as a data type with an equivalence relation – an object usually known as a setoid. The corresponding formalisation of a locally small category is called an E-category.

In Paper I, we show that type theory without universes is insufficient for proving that some expected properties hold of the E-category of setoids, but that a minimal universe is sufficient.

In Paper II, we show that although the collection of all E-categories does not form a category, we can introduce a type-theoretic version of bicategories, and the E-categories form such an E-bicategory.

In Paper III, we consider the setoids inside a type-theoretic universe. The axiom of unique substitutions is proposed and used to show that these form a small category (that is, a category witha setoid of objects and a single setoid of all arrows). We demonstrate that this construction can not be carried out without adding some new axiom to type theory. We also show that the axiom of unique substitutions is strictly weaker than the axiom of unique identity proofs.

In Paper IV, we investigate partial equivalence relations, also known as partial setoids, in Heyting arithmetic in all finite types, and adapt the result that the extensional axiom of choice is equivalent to the combination of the intensional axiom of choice, classical logic, and an extensionality axiom.

In Paper V, we investigate PHL, a logic of partial terms, and prove a cut elimination theorem for it and for a related calculus.

1. Setoids and universes$(function(){PrimeFaces.cw("OverlayPanel","overlay375252",{id:"formSmash:j_idt423:0:j_idt427",widgetVar:"overlay375252",target:"formSmash:j_idt423:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. An E-bicategory of E-categories, exemplifying a type-theoretic approach to bicategories$(function(){PrimeFaces.cw("OverlayPanel","overlay105840",{id:"formSmash:j_idt423:1:j_idt427",widgetVar:"overlay105840",target:"formSmash:j_idt423:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

3. Constructing a small category of setoids$(function(){PrimeFaces.cw("OverlayPanel","overlay451759",{id:"formSmash:j_idt423:2:j_idt427",widgetVar:"overlay451759",target:"formSmash:j_idt423:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

4. PERs in HA^{ω} I: Basic constructions and choice principles$(function(){PrimeFaces.cw("OverlayPanel","overlay447269",{id:"formSmash:j_idt423:3:j_idt427",widgetVar:"overlay447269",target:"formSmash:j_idt423:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

5. Some proof-theoretic properties of PHL and related systems$(function(){PrimeFaces.cw("OverlayPanel","overlay375559",{id:"formSmash:j_idt423:4:j_idt427",widgetVar:"overlay375559",target:"formSmash:j_idt423:4:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1088",{id:"formSmash:lower:j_idt1088",widgetVar:"widget_formSmash_lower_j_idt1088",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1089_j_idt1091",{id:"formSmash:lower:j_idt1089:j_idt1091",widgetVar:"widget_formSmash_lower_j_idt1089_j_idt1091",target:"formSmash:lower:j_idt1089:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});