I agree with FL's and Mario's comments. If one does category theory in a set theoretical framework, then Grothendieck's universes are the way to go. My initial remark "First note that categories as defined in set.mm are small (that is, their morphisms form sets), so there is no size issue to worry about." was there to mean only that: there is no size issue to worry about.
Benoît -- 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/ef56076d-3369-4500-b60a-90efddd9bce5%40googlegroups.com.
