We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Constructing a small category of setoids.
- Authors
WILANDER, OLOV
- Abstract
Consider the first-order theory of a category.d 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.
- Subjects
CONSTRUCTIVE mathematics; CATEGORIES (Mathematics); GROUP theory; PROOF theory; TYPE theory; MATHEMATICAL models; MATHEMATICAL analysis
- Publication
Mathematical Structures in Computer Science, 2012, Vol 22, Issue 1, p103
- ISSN
0960-1295
- Publication type
Article
- DOI
10.1017/S0960129511000478