From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8801 Path: news.gmane.org!not-for-mail From: Toby Bartels Newsgroups: gmane.science.mathematics.categories Subject: Re: Formalizing topos-theoretic arguments in Lean Date: Tue, 19 Jan 2016 03:36:47 +0000 Message-ID: References: Reply-To: Toby Bartels NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1453297907 27334 80.91.229.3 (20 Jan 2016 13:51:47 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 20 Jan 2016 13:51:47 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Wed Jan 20 14:51:33 2016 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.22]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1aLtAa-0004Gc-9X for gsmc-categories@m.gmane.org; Wed, 20 Jan 2016 14:51:32 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:47741) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1aLt9M-0005Gn-D4; Wed, 20 Jan 2016 09:50:16 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1aLt9H-0001H4-4M for categories-list@mlist.mta.ca; Wed, 20 Jan 2016 09:50:11 -0400 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8801 Archived-At: Todd Wilson wrote in part: >this proof does not appear to be well-known, since there is no reference >to it in Section D4.5 of Johnstone's Elephant book or, for example, in >the article on the well-ordering theorem in the nLab It's mentioned there now, since I just added your paper and formalization to the reference list. But it's rare for the nLab to have a comprehensive list of references. This article, for example, despite being begun in 2009, had only Zermelo's original 1904 paper until Thomas Holder added more last year (in 2015). --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]