Replacement in a topos with an eye to a natural model of TST

52 Views Asked by At

TST is a typed first order set theory that is essentially the friendly, simple version of Russell's type theory. There are an infinite number of sorts indexed by the natural numbers, each variable belongs to a fixed sort, and there's a membership predicate $\in_n$ for each sort such that only atomic formulae of the form $x_n \in_n y_{n+1}$ are part of the syntax.

The obvious models of this theory, the natural models, are the ones formed by taking some set as the bottom type, and then type n+1 as the power set of type n. This construction is well known to require some amount of replacement, which is not something easily come by in your average topos.

So my question is primarily for references to the kind of gear one might add to a topos to get better replacement-like features to form something like indexed iterated power objects with a good membership relation. I know it's out there but I just can't seem to track it down!

1

There are 1 best solutions below

1
On BEST ANSWER

There is a variant of ETCS with replacement, due to Colin McLarty, but I don't think this is really the right approach. For instance, for your specific problem of iterating the power object functor, the real issue is not replacement but rather that the induction principle you get out of the universal property of an NNO is too weak. Here's a non-parametrised axiom scheme that will do what you want:

For every $\mathcal{S}$-indexed endofunctor $F : \mathbb{S} \to \mathbb{S}$, there exist a functor $\bar{F} : \mathcal{S} \to \mathcal{S}_{/ N}$ and natural isomorphisms $$z^* \bar{F} X \cong X$$ $$s^* \bar{F} X \cong F^N \bar{F} X$$ for every object $X$ in $\mathcal{S}$, where $(N, z, s)$ is an NNO in $\mathcal{S}$.

Of course, we should really allow ourselves parameters, but the parametrised version is very fiddly to state. More debatable is whether we should generalise from endofunctors defined on all of $\mathbb{S}$ to those defined on only the isomorphisms – the latter would match "large" elimination rules in homotopy type theory more closely.