In response to a request, this page explains how to define a small category using SEAR as foundations. Note that, while SEAR respects the principle of equivalence in that one cannot compare arbitrary sets for equality, it has no provision for small types with no notion of equality. Thus we will be formalising small strict categories, and it will be possible to make statemens about them that do not respect the principle of equivalence.
There are actually two ways to interpret this programme. One is to accept every set in SEAR as ‘small’ and consider categories that are small in that sense. So the category of all SEAR sets cannot be formalised this way, but any category whose set of objects and hom-sets are sets in SEAR can be formalised in this way. Another way is to declare a family of sets within SEAR to be the family of ‘small’ sets; then only categories with a set of morphisms that belongs to this family can be formalised in this way. (This way is even more principle of equivalence-breaking in that one can even consider equality of categories, not only equality of objects within a given category.) There is small category (in the first sense) of all small categories (in the second sense).
We call these two interpretations the ‘large universe’ and ‘small universe’ interpretations.
A category is a syntactic quintuple that consists of
satsifying these conditions:
Note that a partial function from is formalised as a functional relation, that is a relation such that whenever and both hold (for elements of and of ). We say that is defined if there is such that holds; in that case, such is unique and we denote it . This notation can be eliminated from the language using existential quantification, the same as when is a function.
Take a relation as the family of small sets. Then a small category (relatively to this family) is an element of … such that …. Along with the set of small categories, we consider the relations …, which are respectively the families of sets of objects, sets of morphisms, source maps, target maps, and composition maps.
Hopefully it's obvious, but this not completed. It would be nice to carry the development to the point that, given any family of sets, the relatively small categories in this sense form a category in the above sense.