From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8303 Path: news.gmane.org!not-for-mail From: Toby Bartels Newsgroups: gmane.science.mathematics.categories Subject: Re: Uniform locales in Shv(X) Date: Tue, 26 Aug 2014 22:05:30 -0700 Message-ID: References: Reply-To: Toby Bartels NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1409150640 7109 80.91.229.3 (27 Aug 2014 14:44:00 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 27 Aug 2014 14:44:00 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Wed Aug 27 16:43:50 2014 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.1.127]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1XMeRx-0008Oi-NK for gsmc-categories@m.gmane.org; Wed, 27 Aug 2014 16:43:49 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58946) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1XMeQX-0002qY-Pj; Wed, 27 Aug 2014 11:42:21 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1XMeQW-0007GO-Kx for categories-list@mlist.mta.ca; Wed, 27 Aug 2014 11:42:20 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8303 Archived-At: Jeff Egger wrote in part: >I have an idea of how this might be done, but it requires a detour through gauge spaces [...] which I'm not sure is constructively valid. Presumably it's not valid if we don't at least have the classical theorem that every pointwise uniformity comes from a family of psuedometrics. The proof that I know of this relies on dependent choice, as well as forming infima of inhabited sets of nonnegative real numbers. These infima are constructively valid if we allow our pseudometrics to take values in the upper real numbers instead of only the real numbers. I don't know what to do about the dependent choice, however. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]