A strict category is a category together with the structure of a set (or class) on its collection of objects; in particular, the objects can be compared for equality (not merely isomorphism). In contrast, a weak category is a category without such structure. Similarly, a strict functor is one which preserves equality of objects: if . (NB: this is not inherently size-related—both large and small categories can be either strict or weak.)
If we use set-theoretic foundations for category theory, then by definition, a category comes with a set (or class) of objects, and therefore admits the structure of a strict category in a canonical way. Thus, in this case, it is possible to ignore the adjective “strict” in “strict category”, while a “strict functor” simply means a “non-ana functor” (the usual default meaning of ‘functor’, but not necessarily the best concept).
If we additionally assume the (possibly global) axiom of choice, then not only is any category equivalent to a canonical strict category, but every (ana-)functor is naturally isomorphic to a strict functor, so the notions have little to no mathematical content. But in other foundations, these facts may not be true.
Moreover, even in set-theoretic foundations with global , the notion of strict category is not meaningless: calling a category strict signals that we intend to make use of the equality relation on its objects. When taking the nPOV, we often adopt the philosophical position that category theory is fundamentally about weak categories; see the discussion at evil. However, strict categories still do occasionally arise in mathematical practice; see the examples below.
In order to formulate a foundation-independent definition, we make the following assumptions. Ignoring size issues, suppose that we have a bicategory consisting of weak categories, functors (some of which are essentially surjective), and natural transformations (some of which are natural isomorphisms). Suppose also that we have a category consisting of sets and functions, and a functor taking each set to the discrete category on that set. Note that we do not assume the existence of an “underlying set of objects” functor .
In this context, a strict category consists of
A strict functor from to (both strict categories) consists of
Two strict functors are equal if
There is an obvious notion of composition that defines a 1-category of strict categories and (equality classes of) strict functors. Note that this 1-category has a strictly associative and unital composition law, even if is only a bicategory. (However, is not itself a strict category, unless the assumed category is strict.) We have a forgetful functor and a pseudofunctor .
Finally, a natural transformation between two strict functors and is simply
(That is, a natural transformation between strict functors is automatically strict.) With these as 2-cells, we have a strict 2-category of strict categories, strict functors, and natural transformations.
An equivalent definition is that a strict category is an -category whose underlying category of tight morphisms is discrete, while a strict functor is an -functor. In this case, the tight morphisms (which are necessarily isomorphisms) are sometimes called special isomorphisms.
We now make the above schematic definition explicit in terms of various different foundational systems.
In classical set-theoretic foundations including the axiom of choice, we take to be the strict 2-category consisting of (say small) categories, functors, and natural transformations, defined in any of the traditional ways. The functor is left adjoint to the functor , and thus is a subcategory of the Freyd cover of .
In this case, the functor has a right adjoint which takes a category to the strict category . The adjunction counit is literally the identity, while the adjunction unit consists of equivalences (but not isomorphisms) in the strict -category . Thus, is equivalent to (as a bicategory).
The right adjoint also has a further right adjoint defined as follows: given a strict category , let be the category with as its set of objects, and morphisms induced from those in . The unit of this adjunction again consists of identities, while the counit consists of equivalences in .
This analysis applies not only to material set theories such as ZFC, but also structural set theories such as ETCS and SEAR, as long as they have the axiom of choice.
In this case, it is usually best to define Cat to be the bicategory of categories, anafunctors, and natural transformations. Now although every category has an underlying set of objects, we no longer have a functor . It is still true that every category admits the structure of a strict category in a canonical way (with its set of objects), but not every strict category necessarily arises in this way, and not every morphism in (i.e. anafunctor) is a strict functor relative to the canonical strict-category structures of and . In fact, an anafunctor is a strict functor precisely when it is naturally isomorphic to an ordinary (non-ana) functor.
If we instead defined to consist only of non-ana functors, then everything would happen exactly as with AC, except that neither adjunction would be an equivalence.
We include under this heading all theories in which the basic objects, generally called types or presets (and sometimes even called ‘sets’), come with an equality relation, but the notion of set is a defined one. Generally, the issue is that types (or presets) do not admit quotients, and so a set is defined to be a type equipped with an equivalence relation called “equality” (sometimes called a setoid in this context, especially if the types or presets are themselves confusingly called ‘sets’).
In this case, it is natural to define a category to have only a type/preset of objects, but a set(oid) of morphisms between each pair of objects; see type-theoretic definition of category. Now every category still has an underlying set of objects, but not every set is the set of objects underlying some category; only the completely presented sets have this property.
Again, it is true that every category can be made into a strict one in a canonical way, but that not every strict category arises in this way. This is a different sort of failure than in set theory without , and can happen even in the presence of full (even for setoids). For instance, consider the discrete category on the set of real numbers. Of course this depends on specifics, but typically, there is no type of real numbers per se but only a type of Cauchy (pre)sequences of rational numbers (see Cauchy real number). To get the set of real numbers, we must consider this type together with a certain equivalence relation, a setoid. The discrete category on the set of real numbers is essentially the exact same construction, now with a note that parallel morphisms are always defined to be equal. The automatic notion of equality on the objects of this category is equality of Cauchy (pre)sequences, but the desired notion of equality for this discrete category as a strict category is isomorphism, which is equality of real numbers. So while this category may be automatically a strict category, it is a strict category in the wrong way. (This is not a perfect example, since, given , the discrete category of real numbers is still equivalent to the discrete category of Cauchy sequences and therefore does arise as a canonical strict category, up to equivalence.)
Note that we still have a functor which regards an equivalence relation on a type as a groupoid with as its type of objects. The resulting structure of strict categories behaves much like it does in set theory without AC.
If types or presets do not come with a notion of equality, as in some preset theories and SEAR+ε, then a category does not in general even have an “underlying set of objects”, so a category cannot be made into a strict category in any canonical way. But defining sets as presets with equivalence relations as before, we still have , and we can define strict categories, constructing specific examples as wanted.
If type theory is treated as a theory of set-like objects, then it behaves as above, whether extensional or intensional. However, if we take the point of view of homotopy type theory, then the basic objects of the theory are homotopy types, a.k.a. ∞-groupoids. A set is now defined to be an h-set, i.e. a 0-truncated type.
Now the natural definition of (1-)category is something like a complete Segal space, where the type of objects is 1-truncated (a groupoid) and equivalent to the core of the category. Now (even though identity types exist in HoTT), not every category has an underlying set of objects, so again a category cannot be made into a strict category in any canonical way. But again, we still have and we can define strict categories.
In Jean Bénabou’s 1985 paper Fibered categories and the foundations of naive category theory, it is argued that the right notion of a category in/over another category is given by a fibered category , possibly with some additional structure corresponding to the “definability” (representability of certain sieves of ) of equality of parallel pairs, isomorphisms, etc. (See indexed category for more motivation.) In this context, equality of objects is available precisely when the fibration is split.
In particular, if is locally small and has pullbacks, then an internal category object in (in the traditional sense) gives rise to an honest functor and so a split fibration by the Grothendieck construction.
There are some at M-category, to put also here.
The notion of strict category is related to the notion of strictness in higher category theory.
For instance, a 2-category must have strict categories as its hom-categories in order to write down the definition of strict 2-category; a similar remark holds for strict 2-functors. As such, strictness in the sense of this page matches the usual sense of strictness in a “local” sense (every strict 2-category is locally a strict 1-category). However, we now get a notion of strict -natural transformation as a 2-natural transformation? that preserves equality (that is, if two objects are equal, then so are the corresponding components of the natural transformation). (All modifications between strict transformations are automatically strict … until we get to -categories, of course!)
On the other hand, the underlying 1-category of a strict 2-category (its objects and 1-morphisms) need not be a strict 1-category. For instance, this is the case for the strict 2-category defined in a structural set theory, such as SEAR, in which there is no equality predicate on sets. For a fully consistent terminology, we could say ‘locally strict -category’ in place of ‘strict -category’, but this is unlikely to catch on. Some system of numbered strictness (-strict, -strict, etc) might also work.