Mathematical Structures in Computer Science


Setoids and universes


a1 Department of Mathematics, Uppsala University, P.O. Box 480, SE-751 06 Uppsala, Sweden Email: [email protected]


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.

(Received October 28 2008)

(Revised January 15 2010)

(Online publication April 07 2010)


This research was supported by FMB, the Swedish Graduate School in Mathematics and Computing.