Setoids and universes
2010 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 20, no 4, 563-576 p.Article in journal (Refereed) Published
Setoids commonly take the place of sets when formalising mathematics inside type theory. In this note, the category of setoids is studied in type theory with universes that are as small as possible (and thus, the type theory is as weak as possible). In particular, we will consider epimorphisms and disjoint sums. We show that, given the minimal type universe, all epimorphisms are surjections, and disjoint sums exist. Further, without universes, there are countermodels for these statements, and if we use the Logical Framework formulation of type theory, these statements are provably non-derivable.
Place, publisher, year, edition, pages
2010. Vol. 20, no 4, 563-576 p.
IdentifiersURN: urn:nbn:se:uu:diva-135600DOI: 10.1017/S0960129510000071ISI: 000280672800003OAI: oai:DiVA.org:uu-135600DiVA: diva2:375252