The problem with large categories is that they don't fit in as structures. You have to have a completely separate theory for them, so they aren't really categories at all. And category theorists never stop there anyway. They want to make constructions on top of these categories, talking about "conglomerates" and such, and then you are stuck. I think it is better to just always relativize to some set when doing explicit category theory. In theory, TG is there in case we need ZFC in one of these sets, but in practice (at least in the small amount of category theory done thus far) it hasn't been needed at all, and "weak universes" are mostly sufficient and can be proven to exist in ZFC.
On Wed, Jan 29, 2020 at 7:57 AM 'fl' via Metamath <[email protected]> wrote: > > They are small but Tarski-Grothendieck's axiom has been added. that means > that you can > always find sets of sufficient size where all the operations you expect in > set theory are available: > powerset, union etc. So as I understand it, they are small but you will > never notice it. > > However it would be interesting to identify where being small matters. > > I had tried to add an alternate definition where we could deal with not > small categories > but Norm didn't want it. It is reasonable to keep the system sound but > that means there is no > way to understand precisely where smallness occurs precisely in the theory. > > -- > FL > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/b5e0497b-933a-4553-8c7f-b3e14d63aac6%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b5e0497b-933a-4553-8c7f-b3e14d63aac6%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSswBEc6bo91As3-h9bd%3D%3DJaTrv0T47iqzOxvjxAjL_EiA%40mail.gmail.com.
