Constructing a small category of setoids
Olov Wilander · Mathematical Structures in Computer Science · 2011
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 ofunique 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.