From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/10237 Path: news.gmane.io!.POSTED.ciao.gmane.io!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: locales such that the associated topos is subdiscrete? Date: Wed, 10 Jun 2020 12:40:18 +0200 Message-ID: References: Reply-To: Thomas Streicher Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Injection-Info: ciao.gmane.io; posting-host="ciao.gmane.io:159.69.161.202"; logging-data="115139"; mail-complaints-to="usenet@ciao.gmane.io" Cc: "categories@mta.ca" To: Jens Hemelaer Original-X-From: majordomo@rr.mta.ca Wed Jun 10 21:24:07 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 1jj6KU-000Tl9-IM for gsmc-categories@m.gmane-mx.org; Wed, 10 Jun 2020 21:24:06 +0200 Original-Received: from rr.mta.ca ([198.164.44.159]:56302) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1jj6Js-00012p-MI; Wed, 10 Jun 2020 16:23:28 -0300 Original-Received: from majordomo by rr.mta.ca with local (Exim 4.92.1) (envelope-from ) id 1jj6Jn-0004P1-Jd for categories-list@rr.mta.ca; Wed, 10 Jun 2020 16:23:23 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.io gmane.science.mathematics.categories:10237 Archived-At: 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/ ]