categories in SEAR

Categories in SEAR


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.

Large universe version

A category is a syntactic quintuple that consists of

  • a set OO (called the set of objects),
  • a set MM (called the set of morphisms),
  • a function s:MOs: M \to O (the source map),
  • a function t:MOt: M \to O (the target map),
  • and a partial function c:M×MMc: M \times M \dashrightarrow M (the composition map)

satsifying these conditions:

  • For f,gf, g elements of MM, c(f,g)c(f,g) is defined if and ony if s(f)=t(g)s(f) = t(g).
  • In that case, s(c(f,g))=s(g)s(c(f,g)) = s(g) and t(c(f,g))=t(f)t(c(f,g)) = t(f).
  • For every element xx of OO, there exists an element ii of MM such that
    • s(i)=xs(i) = x and t(i)=xt(i) = x,
    • c(i,f)=fc(i,f) = f for every element ff of MM such that x=t(f)x = t(f), and
    • c(f,i)=fc(f,i) = f for every element ff of MM such that s(f)=xs(f) = x.
  • For f,g,hf, g, h elements of MM such that s(f)=t(g)s(f) = t(g) and s(g)=t(h)s(g) = t(h), we have c(c(f,g),h)=c(f,c(g,h))c(c(f,g),h) = c(f,c(g,h)).

Note that a partial function from p:XYp: X \dashrightarrow Y is formalised as a functional relation, that is a relation ϕ:XY\phi: X \to Y such that b=cb = c whenever ϕ(a,b)\phi(a,b) and ϕ(a,c)\phi(a,c) both hold (for elements aa of XX and b,cb,c of YY). We say that p(x)p(x) is defined if there is yy such that ϕ(x,y)\phi(x,y) holds; in that case, such yy is unique and we denote it p(x)p(x). This notation can be eliminated from the language using existential quantification, the same as when pp is a function.

Small universe version

Take a relation m:UEm : U \looparrowright E 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.

Revised on April 22, 2017 05:59:23 by Urs Schreiber (