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

Constructions of categories of setoids from proof-irrelevant familiesPrimeFaces.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)In: Archive for mathematical logic, ISSN 0933-5846, E-ISSN 1432-0665, Vol. 56, no 1-2, p. 51-66Article in journal (Refereed) Published
##### Abstract [en]

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

2017. Vol. 56, no 1-2, p. 51-66
##### Keyword [en]

Martin–Löf type theory Proof-irrelevance Category
##### National Category

Mathematics
##### Research subject

Mathematical Logic
##### Identifiers

URN: urn:nbn:se:su:diva-151872DOI: 10.1007/s00153-016-0514-7OAI: oai:DiVA.org:su-151872DiVA, id: diva2:1176010
#####

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

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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt620",{id:"formSmash:j_idt620",widgetVar:"widget_formSmash_j_idt620",multiple:true});
##### Funder

Swedish Research Council
Available from: 2018-01-19 Created: 2018-01-19 Last updated: 2018-01-26Bibliographically approved

When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Löf type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family *F* of setoids. The objects of the categories form the index setoid *I* of the family, whereas the definition of arrows differs. The first category has for arrows triples (a,b,f:F(a)→F(b))" role="presentation">(a,b,f:F(a)→F(b)) where *f* is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by *F*) makes them equal. In the second category the arrows are triples (a,b,R↪Σ(I,F)2)" role="presentation">(a,b,R↪Σ(I,F)2) where *R* is a total functional relation between the subobjects F(a),F(b)↪Σ(I,F)" role="presentation">F(a),F(b)↪Σ(I,F) of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category.

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

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