From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10256 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: ptj@maths.cam.ac.uk Newsgroups: gmane.science.mathematics.categories Subject: Re: locales such that the associated topos is subdiscrete? Date: 22 Jul 2020 10:14:06 +0100 Message-ID: References: Reply-To: ptj@maths.cam.ac.uk Mime-Version: 1.0 Content-Type: text/plain; format=flowed; charset=ISO-8859-1 Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="14027"; mail-complaints-to="usenet@ciao.gmane.io" Cc: "categories@mta.ca" To: Thomas Streicher Original-X-From: majordomo@rr.mta.ca Wed Jul 22 16:03:21 2020 Return-path: Envelope-to: gsmc-categories@m.gmane-mx.org Original-Received: from smtp2.mta.ca ([198.164.44.55]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1jyFL6-0003VX-T1 for gsmc-categories@m.gmane-mx.org; Wed, 22 Jul 2020 16:03:21 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:60740) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1jyFKk-0001S0-AF; Wed, 22 Jul 2020 11:02:58 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1jyFKW-0003wL-OY for categories-list@rr.mta.ca; Wed, 22 Jul 2020 11:02:44 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10256 Archived-At: On Jun 10 2020, Thomas Streicher wrote: >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 > > This is NOT an open question, despite being stated as such in Jaap van Oosten's book; indeed, I knew the answer before Ieke raised the question at Jaap's PhD viva (but Ieke never bothered to ask me ...). There is a proof in my paper "Geometric morphisms of realizability toposes", TAC 28 (2013), 241. Peter Johnstone [For admin and other information see: http://www.mta.ca/~cat-dist/ ]