Return to Answer

Your long question suggested at first that you were asking for something difficult (a locally full internal topos), but you ended up asking for the easy thing.

Starting from your postscript, the purpose of an arithmetic universe is that it is is the least categorical structure in which one can construct the free or initial structure of a widely applicable kind, namely essentially algebraic. (See my answer here for a brief explanation of arithmetic universes.) Any elementary topos with natural numbers object is an arithmetic universe.

The structure of an elementary topos (with natural numbers if you wish) is essentially algebraic, so

There is an initial elementary topos with natural numbers in any arithmetic universe, in particular in any elementary topos with natural numbers.

I would like to refer you to the books 2-Categories for the Working Categorist and Introduction to Arithmetic Universes, but regrettably nobody has written them yet.

Talking about ZFC or cumulative hierarchies in this is really obfuscation. However, I indicated how to build the set-theoretic hierarchy in my paper Intuitionistic Sets and Ordinals, based on earlier ideas of Gerhard Osius.

As François Dorais points out above, the initial model may be degenerate, just as it may be in any situation in logic or algebra, and so much more difficult questions of consistency or incompleteness arise. Indeed, André Joyal proved Gödel's incompleteness theorem categorically in the following form:

In the initial arithmetic universe $\mathcal A$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the initial object $\mathbf 0$ of $\mathcal A$.

On the other hand, again as in traditional logic, if the outer structure is of a stronger kind than the inner one then there are methods of proving internal consistency.

For example, the natural numbers provide a bare-hands model of set theory (without inifinity), in which $n\epsilon m$ if the $n$th binary digit of $m$ is $1$, and so a Boolean internal elementary topos.

A particularly neat and powerful method is the gluing construction (known in computer science as logical relations); for my account of this see Section 7.7 of my book.

Your long question suggested at first that you were asking for something difficult (a locally full internal topos), but you ended up asking for the easy thing.

Starting from your postscript, the purpose of an arithmetic universe is that it is is the least categorical structure in which one can construct the free or initial structure of a widely applicable kind, namely essentially algebraic. (See my answer here for a brief explanation of arithmetic universes.) Any elementary topos with natural numbers object is an arithmetic universe.

The structure of an elementary topos (with natural numbers if you wish) is essentially algebraic, so

There is an initial elementary topos with natural numbers in any arithmetic universe, in particular in any elementary topos with natural numbers.

I would like to refer you to the books 2-Categories for the Working Categorist and Introduction to Arithmetic Universes, but regrettably nobody has written them yet.

Talking about ZFC or cumulative hierarchies in this is really obfuscation. However, I indicated how to build the set-theoretic hierarchy in my paper Intuitionistic Sets and Ordinals, based on earlier ideas of Gerhard Osius.

As François Dorais points out above, the initial model may be degenerate, just as it may be in any situation in logic or algebra, and so much more difficult questions of consistency or incompleteness arise. Indeed, André Joyal proved Gödel's incompleteness theorem categorically in the following form:

In the initial arithmetic universe $\mathcal A$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the initial object $\mathbf 0$ of $\mathcal A$.

On the other hand, again as in traditional logic, if the outer structure is of a stronger kind than the inner one then there are methods of proving internal consistency.

For example, the natural numbers provide a bare-hands model of set theory (without inifinity), in which $n\epsilon m$ if the $n$th binary digit of $m$ is $1$, and so a Boolean internal elementary topos.

A particularly neat and powerful method is the gluing construction (known in computer science as logical relations); for my account of this see Section 7.7 of my book.

Your long question suggested at first that you were asking for something difficult (a locally full internal topos), but you ended up asking for the easy thing.

Starting from your postscript, the purpose of an arithmetic universe is that it is is the least categorical structure in which one can construct the free or initial structure of a widely applicable kind, namely essentially algebraic. (See my answer here for a brief explanation of arithmetic universes.)

The structure of an elementary topos (with natural numbers if you wish) is essentially algebraic, so

there is an initial elementary topos with natural numbers in any arithmetic universe, in particular in any elementary topos with natural numbers.

I would like to refer you to the books 2-Categories for the Working Categorist and Introduction to Arithmetic Universes, but regrettably nobody has written them yet.

Talking about ZFC or cumulative hierarchies in this is really obfuscation. However, I indicated how to build the set-theoretic hierarchy in my paper Intuitionistic Sets and Ordinals, based on earlier ideas of Gerhard Osius.

As François Dorais points out above, the initial model may be degenerate, just as it may be in any situation in logic or algebra, and so much more difficult questions of consistency or incompleteness arise. Indeed, André Joyal proved Gödel's incompleteness theorem categorically in the following form:

in the initial arithmetic universe $\mathcal A$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the inital object $\mathbf 0$ of $\mathcal A$

On the other hand, again as in traditional logic, if the outer structure is of a stronger kind than the inner one then there are methods of proving internal consistency.

For example, the natural numbers provide a bare-hands model of set theory (without inifinity), in which $n\epsilon m$ if the $n$th binary digit of $m$ is $1$, and so a Boolean internal elementary topos.

A particularly neat and powerful method is the gluing construction (known in computer science as logical relations); for my account of this see Section 7.7 of my book.

Your long question suggested at first that you were asking for something difficult (a locally full internal topos), but you ended up asking for the easy thing.

Starting from your postscript, the purpose of an arithmetic universe is that it is is the least categorical structure in which one can construct the free or initial structure of a widely applicable kind, namely essentially algebraic. (See my answer here for a brief explanation of arithmetic universes.) Any elementary topos with natural numbers object is an arithmetic universe.

The structure of an elementary topos (with natural numbers if you wish) is essentially algebraic, so

There is an initial elementary topos with natural numbers in any arithmetic universe, in particular in any elementary topos with natural numbers.

I would like to refer you to the books 2-Categories for the Working Categorist and Introduction to Arithmetic Universes, but regrettably nobody has written them yet.

Talking about ZFC or cumulative hierarchies in this is really obfuscation. However, I indicated how to build the set-theoretic hierarchy in my paper Intuitionistic Sets and Ordinals, based on earlier ideas of Gerhard Osius.

As François Dorais points out above, the initial model may be degenerate, just as it may be in any situation in logic or algebra, and so much more difficult questions of consistency or incompleteness arise. Indeed, André Joyal proved Gödel's incompleteness theorem categorically in the following form:

In the initial arithmetic universe $\mathcal A$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the initial object $\mathbf 0$ of $\mathcal A$.

On the other hand, again as in traditional logic, if the outer structure is of a stronger kind than the inner one then there are methods of proving internal consistency.

For example, the natural numbers provide a bare-hands model of set theory (without inifinity), in which $n\epsilon m$ if the $n$th binary digit of $m$ is $1$, and so a Boolean internal elementary topos.

A particularly neat and powerful method is the gluing construction (known in computer science as logical relations); for my account of this see Section 7.7 of my book.

Your long question suggested at first that you were asking for something difficult (a locally full internal topos), but you ended up asking for the easy thing.

Starting from your postscript, the purpose of an arithmetic universe is that it is is the least categorical structure in which one can construct the free or initial structure of a widely applicable kind, namely essentially algebraic. (See my answer here for a brief explanation of arithmetic universes.)

The structure of an elementary topos (with natural numbers if you wish) is essentially algebraic, so there is an initial elementary topos with natural numbers in any arithmetic universe, in particular in any elementary topos with natural numbers.

I would like to refer you to the books 2-Categories for the Working Categorist and Introduction to Arithmetic Universes, but regrettably nobody has written them yet.

Talking about ZFC or cumulative hierarchies in this is really obfuscation. However, I indicated how to build the set-theoretic hierarchy in my paper Intuitionistic Sets and Ordinals, based on earlier ideas of Gerhard Osius.

Your long question suggested at first that you were asking for something difficult (a locally full internal topos), but you ended up asking for the easy thing.

Starting from your postscript, the purpose of an arithmetic universe is that it is is the least categorical structure in which one can construct the free or initial structure of a widely applicable kind, namely essentially algebraic. (See my answer here for a brief explanation of arithmetic universes.)

The structure of an elementary topos (with natural numbers if you wish) is essentially algebraic, so

there is an initial elementary topos with natural numbers in any arithmetic universe, in particular in any elementary topos with natural numbers.

I would like to refer you to the books 2-Categories for the Working Categorist and Introduction to Arithmetic Universes, but regrettably nobody has written them yet.

Talking about ZFC or cumulative hierarchies in this is really obfuscation. However, I indicated how to build the set-theoretic hierarchy in my paper Intuitionistic Sets and Ordinals, based on earlier ideas of Gerhard Osius.

As François Dorais points out above, the initial model may be degenerate, just as it may be in any situation in logic or algebra, and so much more difficult questions of consistency or incompleteness arise. Indeed, André Joyal proved Gödel's incompleteness theorem categorically in the following form:

in the initial arithmetic universe $\mathcal A$, the internal hom-object $A(1,0)$ of its internal initial arithmetic universe $A$ (where $0,1:{\mathbf 1}\rightrightarrows A$ are the internal initial and terminal objects of $A$) is not isomorphic to the inital object $\mathbf 0$ of $\mathcal A$

On the other hand, again as in traditional logic, if the outer structure is of a stronger kind than the inner one then there are methods of proving internal consistency.

For example, the natural numbers provide a bare-hands model of set theory (without inifinity), in which $n\epsilon m$ if the $n$th binary digit of $m$ is $1$, and so a Boolean internal elementary topos.

A particularly neat and powerful method is the gluing construction (known in computer science as logical relations); for my account of this see Section 7.7 of my book.