Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: type-theoretic replacement

Leopold Schlicht (Aug 23 2021 at 18:26):

@Ulrik Buchholtz Thanks!

Not directly related: I think another candidate for a type-theoretical "replacement axiom" would be the rule stating that $\sum_{i\colon I} A_i\colon\mathcal U$ whenever $i\colon I\vdash A_i\colon\mathcal U$ and $I\colon\mathcal U$. Is there some way of making precise the idea that this (or any other type-theoretical statement) is the type-theoretical replacement axiom? Of course, in a material set theory, replacement implies that the universe is closed under arbitrary coproducts. But it might not be equivalent to this statement and imply a lot of other things. However, the hope would be that this statement somehow captures all "structural" or "type-theoretical" applications of the replacement axiom. (Maybe Ulrik's replacement principle is a counterexample?)

Mike Shulman (Aug 24 2021 at 03:03):

Whenever you find yourself saying "Not directly related..." that's usually a good clue that you should create a new topic. (-:

Mike Shulman (Aug 24 2021 at 03:04):

Leopold Schlicht said:

I think another candidate for a type-theoretical "replacement axiom" would be the rule stating that $\sum_{i\colon I} A_i\colon\mathcal U$ whenever $i\colon I\vdash A_i\colon\mathcal U$ and $I\colon\mathcal U$.

I agree. Some evidence for this is that in set-theoretic semantics, a universe defined by some cardinal is closed under sigmas (and pis) if and only if its cardinality is inaccessible, hence in particular satisfies a relative form of replacement.

I'm not sure why some people have taken to referring to the other thing that Ulrik quoted as "replacement". To me it feels more like a sort of "fracture" or "extension" theorem: if a type is small at dimension 0, and small above dimension 0, then it is small overall.

Ulrik Buchholtz (Aug 24 2021 at 14:48):

That's why I tried to be careful above in not claiming any formal connection. Indeed, it's tricky to make formal comparisons when the systems are so different, something that also came up in the n-Category Café discussions on replacement here, here, and here.

But consider the cumulative hierarchy $V$ as in the HoTT book, relative to a universe $\mathcal{U}$. This is a large, but locally $\mathcal{U}$-small type. As a special case of Egbert's replacement principle, we get that the image of any function $f : A \to V$ from $A:\mathcal{U}$ is essentially $\mathcal{U}$-small. (In fact, this is observed in the book.) If we take $A$ to be the extension of some $a:V$, this is almost literally the set-theoretic replacement axiom.

Also of note, I think, is that it's $\mathcal{U}$-small separation (HoTT book, Thm. 10.5.8(ix)), and not replacement, that requires $\mathcal{U}$ to be closed under $\Sigma$-types.

Leopold Schlicht (Aug 24 2021 at 15:40):

Leinster's blog post "Large Sets 12" is a good read, thanks! I keep wondering: does McLarty's structural replacement axiom suffice for all applications of material-replacement (to proving structural statements)? I guess it could be hard to make that precise, as the formal systems are so different, as Ulrik says, but is there at least some empirical evidence that everything one can prove using the classical material-replacement axiom can be proved using McLarty's replacement?
(EDIT: Maybe that's covered by the biinterpretability between ZFC and ETCS+R Leinster mentions, but only if the interpretations are natural, and I don't know if this is the case.)

Fawzi Hreiki (Aug 24 2021 at 15:48):

I’ve always wondered about this. If you want replacement in an ETCS-type framework, isn’t it much cleaner to have some sort of two level axiomatisation where the meta-theory is (say) a Boolean pretopos in which there is a model of ETCS.

Fawzi Hreiki (Aug 24 2021 at 15:49):

Then ‘sets’ (ie objects internal to the ETCS model) can be ‘externalised’ to ‘collections’ (objects of the pretopos) by homming with the terminal set.

Fawzi Hreiki (Aug 24 2021 at 15:50):

Replacement then just says that families of sets parametrised by small collections (externalisations of sets) are representable in the category of sets.

Mike Shulman (Aug 25 2021 at 07:54):

Ulrik Buchholtz said:

But consider the cumulative hierarchy $V$ as in the HoTT book, relative to a universe $\mathcal{U}$. This is a large, but locally $\mathcal{U}$-small type. As a special case of Egbert's replacement principle, we get that the image of any function $f : A \to V$ from $A:\mathcal{U}$ is essentially $\mathcal{U}$-small. (In fact, this is observed in the book.) If we take $A$ to be the extension of some $a:V$, this is almost literally the set-theoretic replacement axiom.

Surely this proof also uses somewhere that $\mathcal{U}$ is closed under $\Sigma$-types? Assuming so, it seems more reasonable to me even here to attribute the name "replacement" backwards to that property, since Egbert's property is not after all a rule or axiom but a theorem, whereas closure of $\mathcal{U}$ under $\Sigma$-types is a postulated rule.

Mike Shulman (Aug 25 2021 at 08:01):

Leopold Schlicht said:

does McLarty's structural replacement axiom suffice for all applications of material-replacement (to proving structural statements)?

As you say, at a formal level you can always translate to ZFC and back, so technically the answer is yes. But the real question is whether it can be done directly. I would say that it suffices for most applications -- Leinster's blog post gives some evidence in this direction as well. But there are a few sorts of arguments in ZFC that use replacement -- and often also the axiom of foundation -- that it's unclear how to reproduce directly in ETCS+R, such as Scott's trick.

Mike Shulman (Aug 25 2021 at 08:03):

Fawzi Hreiki said:

If you want replacement in an ETCS-type framework, isn’t it much cleaner to have some sort of two level axiomatisation where the meta-theory is (say) a Boolean pretopos in which there is a model of ETCS.

Well, "cleaner" is in the eye of the beholder. One might argue contrariwise that introducing a whole extra level of metatheory and internalization just to get replacement is rather messy. But you can certainly do this, and for a while there was a whole project of studying such "categories of classes" that went by the name algebraic set theory.

Leopold Schlicht (Aug 25 2021 at 15:01):

Thanks!