Re: locales such that the associated topos is subdiscrete?

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

As I was just told by Matias Menni an answer to my question is also
provided in Prop.6.3.5 of Pieter Hofstra's Thesis.

Maybe I should explain a bit why I asked this question. In
arxiv:2005.06019 Jonas Frey and I have characterized triposes over a
base topos SS as regular functors F from SS to a topos EE such that

1. every object of EE appears as subquotient of some FI
2. F^*Sub_EE admits a generic family.

What we had to leave as an open question whether triposes over SS = Set
inducing the same topos are equivalent. In Hyland, Johnstone and Pitts's
paper introcing triposes this question was aked for localic toposes
and remained unanswered since the last 40 years.
Krivine's work on classical realizability has come up with an
alternative characterization of boolean triposes over Set and he has
shown that F : Set->EE is the inverse image part of a localic g.m. iff
F preserves 2. But it is still open whether (boolean) triposes F : Set->EE
with EE loclic are nevessarily isomorphic to Delta : Set -> EE.

BTW if one drops condition 2 there is a simple answer. For natural
numbers n > 0 the functors F_n : Set->Set sending X to X^n are all
triposes in this weaker sense and pairwise not isomorphic. As explained
in my Paper with Jonas these generalized triposes are precisely those
introduced by Andy Pitts in his 1999 paper "Tripos Theory in Retrospect".
In many respects this weaker notion is more natural. The only
disadvantage is that less is expressible in the internal language of
the base topos SS.

Thomas



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