Slate - Categories

Definition 4.1. Let u ∈ ℕ. We define:

Cat_u :=: {[O(M_A,B)_{A,B ∈ O}(i_C)_C ∈ O(∘_D,E,F)_{D,E,F ∈ O}]_u | O is a set, M_A,B is a set for each A, B ∈ O, i_C ∈ M_C,C for each C ∈ O, ∘_D,E,F : M_E,F × M_D,E → M_D,F is an operation for each D, E, F ∈ O, [∀ W, X, Y, Z ∈ O, f ∈ M_W,X, g ∈ M_X,Y, h ∈ M_Y,Z : (h ∘_X,Y,Z g) ∘_W,X,Z f = h ∘_W,Y,Z (g ∘_W,X,Y f)], [∀ X, Y ∈ O, f ∈ M_X,Y : i_Y ∘_X,Y,Y f = f ∘_X,X,Y i_X = f], [∀ X, Y ∈ O s.t. [∃ f ∈ M_X,Y, g ∈ M_Y,X : [f ∘_Y,X,Y g = i_Y and g ∘_X,Y,X f = i_X]] : X = Y]}

[O(M_A,B)_{A,B ∈ O}(i_C)_C ∈ O(∘_D,E,F)_{D,E,F ∈ O}]_u = [P(N_A,B)_{A,B ∈ P}(j_C)_C ∈ P(∙_D,E,F)_{D,E,F ∈ P}]_u :⇔ ∃ φ : O ↔ P, ψ_A,B : M_A,B ↔ N_φ(A),φ(B) f.e. A, B ∈ O : [[∀ C ∈ O : i_C ≃^ψ_C,C j_φ(C)] and ∀ D, E, F ∈ O : ∘_D,E,F ≃^{ψ_E,F,ψ_D,E,ψ_D,F} ∙_{φ(D),φ(E),φ(F)}] (O is a set, M_A,B is a set for each A, B ∈ O, i_C ∈ M_C,C for each C ∈ O, ∘_D,E,F : M_E,F × M_D,E → M_D,F is an operation for each D, E, F ∈ O, P is a set, N_A,B is a set for each A, B ∈ P, j_C ∈ N_C,C for each C ∈ P, ∙_D,E,F : N_E,F × N_D,E → N_D,F is an operation for each D, E, F ∈ P with suitable conditions)

We write “let C be a/an u-small category” for “let C ∈ Cat_u.”

Remarks.

This definition of categories includes the additional requirement that all categories are skeletal. The reasoning behind this is that I expect the equality definition above, which is derived purely syntactically, to be equivalent to isomorphism of categories, not equivalence. That is, without this restriction, two isomorphic categories would be considered equal, but two equivalent categories would not necessarily be. (This needs to be verified.)

For skeletal categories, the two concepts coincide. Since in HLM, all of the usual examples of categories happen to be skeletal anyway, and we care about equivalence much more than isomorphism, it makes sense to include this requirement directly in the definition of a category.

The natural number u is required to be able to define a category of (smaller) categories or functors, which would otherwise be prevented by non-circularity rules. Informally, u can be regarded as a "universe size" that is relevant only in the context of category theory. (The "universes" that are implicit in other contexts are already large enough.)

References.