Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Added reference to the paper
Paul Blain Levy, Formulating Categorical Concepts using Classes, arXiv:1801.08528
What kind of properties can we expect from the “category” of classes in ZFC? In general, power objects do not exist because of Russell’s paradox, but what about (co)limits (not necessarily small) and exponentials?
It’s a model of algebraic set theory.
Dmitri, the category of classes is a pretopos (you can perform first-order logic internally). Exponentials are of course problematic unless one plays games with universes.
To expand on my comment: you have a Boolean pretopos with a subobject classifier, and sets are exponentiable. More generally, I think dependent product exists along maps whose fibres are sets. You can define finite coproducts by taking the disjunction of the formulas defining the sets. Taking infinite coproducts requires infinite disjunctions. Essentially one is using Separation and carving out a subclass of , so need to be able to express the condition to be in the colimit you’re constructing using first-order logic, or whatever you wish to use.
Here is an old M.SE question of mine on the issue. In particular, I eventually found this source that lays things out nicely.
For equivalence relations, if we think of them as internal groupoids in the category of ZF-classes (no choice necessary here), then Scott’s trick cooks up a subgroupoid that is weakly equivalent, and such that each orbit consists of a set. This then has a quotient, for instance because the resulting equivalence relation is classified via a function to the power class of subsets, and the image of this function is a quotient of the new equivalence relation, and hence of the old one. I’m not sure it’s a Boolean vs Heyting thing, but it might manifest itself via the indexing of the cumulative hierarchy, which is what Scott’s trick relies on.
More subtle is if one can generate an equivalence relation from a general (wlog symmetric reflexive) relation. This relies I think on knowing that one can take countable nested unions of subclasses of a fixed class. I’m not sure how to do this.
Re #3: algebraic set theory.
Am I correct that classes in ZFC admit all small colimits, via Scott’s trick? What about small limits?
On a second thought, the notion of a small diagram D:I→Class of classes must be defined carefully. I guess one could say that we have a map of classes T→Ob(I), with the fiber over i∈I being the value of D(i). This essentially postulates the existence of small coproducts by definition.
Re #7: I do not understand why the case of arbitrary class relations is different from class equivalence relations. Given a relation R⊂C⨯C, where C is a proper class, we can define another relation S⊂C⨯C by postulating that S(x,y) holds for x,y∈C if there is a subset A⊂C together with a map g:[0,n]→A such that R(g(i),g(i+1)) holds for all i∈[0,n) and g(0)=x, g(n)=y. This defines the transitive closure of any class relation.
@Dmitri I thought of something like that, but wasn’t convinced at the time. Thanks for an independent check. Note that one doesn’t really need the subset , since functions are meaningful in ZFC.
Added section on finite colimits of external diagrams. We need to tighten up the claim around Scott’s trick for coequalisers in an arbitrary category of classes. One needs a cumulative hierarchy to make this work, or more generally some stratification into sets with a well-founded indexing class.
Added section on finite colimits of external diagrams. We need to tighten up the claim around Scott’s trick for coequalisers in an arbitrary category of classes. One needs a cumulative hierarchy to make this work, or more generally some stratification into sets with a well-founded indexing class.
added the definition of “class” in type theory as an arbitrary modal operator (isn’t required to be idempotent or monadic) on a set-level type theory which takes sets/types to h-propositions.
Anonymous
added the definition of class in type theory, where the propositions as types interpretation is used.
Anonymous
1 to 26 of 26