Constructing a small category of setoids
2012 (English)In: Mathematical Structures in Computer Science, ISSN 0960-1295, E-ISSN 1469-8072, Vol. 22, no 1, 103-121 p.Article in journal (Refereed) Published
Consider the first-order theory of a category. It has a sort of objects, and a sort of arrows (so we may think of it as a small category). We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe provide a model for this first-order theory. We also show that the principle of unique substitutions is not derivable in type theory, but that it is strictly weaker than the principle of unique identity proofs.
Place, publisher, year, edition, pages
2012. Vol. 22, no 1, 103-121 p.
Algebra and Logic
Research subject Mathematical Logic
IdentifiersURN: urn:nbn:se:uu:diva-160604DOI: 10.1017/S0960129511000478ISI: 000299654600005OAI: oai:DiVA.org:uu-160604DiVA: diva2:451759