Re: Reply to Eduardo Dubuc

[David Roberts <david.roberts@adelaide.edu.au>]

Hi,

Since my answer on MathOverflow has been invoked a couple of times,
let me expand on it a little.

There is a notion of a topos being *constructively* well-pointed,
which I learned from Mike Shulman (or rather, his paper Stack
semantics and the comparison of material and structural set theories).
This is the sort of thing that the category of CZF-sets has. And Mike
proved that in the internal logic (in fact in an extension of the
usual one, to cope with unbounded quantifiers), every topos is
constructively well-pointed.

Since Eduardo, at the beginning of his question stated that he was
going to work in the internal logic of the base topos, I took this as
given. Then one can reason as if one has an object * playing the rôle
of the point which picks out elements of 'sets'. The definition of
epimorphism in the internal logic is just that any generalised element
in the codomain lifts to the domain, and this reduces to checking for
elements using *. The coproduct causes no trouble, being indexed by a
'set', and disjoint union doesn't go awry in the intuitionistic
setting, by virtue of the fact coproducts are disjoint in a topos.

To address the point about unbounded quantifiers, Mike gives the
notion of a topos being *autological*, which means that in the
internal logic one has unbounded separation, and so as much of set
theory as one gets from e.g. ZF in the classical case. Given an
autological base topos SS, all locally small cocomplete toposes over
SS are autological, including unbounded ones.

Mike might be able to answer more specific questions people have, but
that is my line of reasoning.

Best,

David

On 29 July 2013 00:50, Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
> Dear David,
>
> indeed Michael's work is an alternative to the AST approach taylored
> towards a setting where it is forbidden to speak of equality of sets.
> He doesn't construct the category of classes around a topos but rather
> works with Kripke Joyal semantics for it.
>
> Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]