you can define to be the 2-category of all -small categories, where is some Grothendieck universe containing . That way, you have without contradiction.
Do you agree with changing this to
” you can define to be the 2-category of all -small categories, where is some Grothendieck universe containing . That way, for every small category , you have the category an object of without contradiction. This way, e.g. the diagram in Cat used in this definition of comma categories is defined. “
?
Reason: motivation is to have the pullback-definition of a comma category in (For others, it’s about the diagram here) defined, or rather, having Cat provide a way to make it precise. Currently, the diagrammatic definition can either be read formally, as a device to encode the usual definition of comma categories, or a reader can try to consult Cat in order to make it precise. Then they will first find only the usual definition of Cat having small objects only, which does not take care of the large category
used in the pullback-definition. Then perhaps they will read all the way up to Grothendieck universes, but find that option not quite sufficient either since it only mentions Set, but not . It seems to me that large small-presheaf-categories such as can be accomodated, too, though.
(Incidentally, tried to find a “canonical” thread for the article “Cat”, by using the search, but to no avail. Therefore started this one.)
]]>