Skip to main content
added 78 characters in body
Source Link
Zhen Lin
  • 15.9k
  • 1
  • 46
  • 84

The effective topos is an example of a (locally!) cartesian closed category with NNO where infinite coproducts do not exist. Indeed, the main feature of the NNO $N$ in the effective topos is that the endomorphisms of $N$ are precisely the computable functions. As such, $N$ cannot be (isomorphic to) $\coprod_{n \in \mathbb{N}} 1$: if that were the case, then there would be uncountably many endomorphisms of $N$. (Of course, $\coprod_{n \in \mathbb{N}} 1$ does not even exist in the effective topos; as you say, if it existed, it would have to be the NNO.)

More generally, supposeHere is a closely related construction. Suppose we have a countable model $M$ of ZF (orZermelo set theory, or even just Mac Lane set theory). (For instance, where by non-standard I mean one with non-standard natural numbersSkolem, we may take $M$ to be a countable elementary substructure of $V_{\omega + \omega}$.) Then the category of sets in $M$ is an elementary topos (so locally cartesian closed) with NNO, but its NNO cannot be $\coprod_{n \in \mathbb{N}} 1$, for the same reason.

The effective topos is an example of a (locally!) cartesian closed category with NNO where infinite coproducts do not exist. Indeed, the main feature of the NNO $N$ in the effective topos is that the endomorphisms of $N$ are precisely the computable functions. As such, $N$ cannot be (isomorphic to) $\coprod_{n \in \mathbb{N}} 1$: if that were the case, then there would be uncountably many endomorphisms of $N$. (Of course, $\coprod_{n \in \mathbb{N}} 1$ does not even exist in the effective topos; as you say, if it existed, it would have to be the NNO.)

More generally, suppose we have a countable model $M$ of ZF (or even just Mac Lane set theory), where by non-standard I mean one with non-standard natural numbers. Then the category of sets in $M$ is an elementary topos (so locally cartesian closed) with NNO, but its NNO cannot be $\coprod_{n \in \mathbb{N}} 1$, for the same reason.

The effective topos is an example of a (locally!) cartesian closed category with NNO where infinite coproducts do not exist. Indeed, the main feature of the NNO $N$ in the effective topos is that the endomorphisms of $N$ are precisely the computable functions. As such, $N$ cannot be (isomorphic to) $\coprod_{n \in \mathbb{N}} 1$: if that were the case, then there would be uncountably many endomorphisms of $N$. (Of course, $\coprod_{n \in \mathbb{N}} 1$ does not even exist in the effective topos; as you say, if it existed, it would have to be the NNO.)

Here is a closely related construction. Suppose we have a countable model $M$ of Zermelo set theory, or even just Mac Lane set theory. (For instance, by Skolem, we may take $M$ to be a countable elementary substructure of $V_{\omega + \omega}$.) Then the category of sets in $M$ is an elementary topos (so locally cartesian closed) with NNO, but its NNO cannot be $\coprod_{n \in \mathbb{N}} 1$, for the same reason.

Source Link
Zhen Lin
  • 15.9k
  • 1
  • 46
  • 84

The effective topos is an example of a (locally!) cartesian closed category with NNO where infinite coproducts do not exist. Indeed, the main feature of the NNO $N$ in the effective topos is that the endomorphisms of $N$ are precisely the computable functions. As such, $N$ cannot be (isomorphic to) $\coprod_{n \in \mathbb{N}} 1$: if that were the case, then there would be uncountably many endomorphisms of $N$. (Of course, $\coprod_{n \in \mathbb{N}} 1$ does not even exist in the effective topos; as you say, if it existed, it would have to be the NNO.)

More generally, suppose we have a countable model $M$ of ZF (or even just Mac Lane set theory), where by non-standard I mean one with non-standard natural numbers. Then the category of sets in $M$ is an elementary topos (so locally cartesian closed) with NNO, but its NNO cannot be $\coprod_{n \in \mathbb{N}} 1$, for the same reason.