From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9008 Path: news.gmane.org!.POSTED!not-for-mail From: Patrik Eklund Newsgroups: gmane.science.mathematics.categories Subject: Re: Grothendieck toposes Date: Thu, 03 Nov 2016 13:13:38 +0200 Message-ID: References: Reply-To: Patrik Eklund NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit X-Trace: blaine.gmane.org 1478195763 11681 195.159.176.226 (3 Nov 2016 17:56:03 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Thu, 3 Nov 2016 17:56:03 +0000 (UTC) Cc: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Thu Nov 03 18:55:56 2016 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.28]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1c2MEY-0007hN-G2 for gsmc-categories@m.gmane.org; Thu, 03 Nov 2016 18:55:26 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:33973) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1c2MEA-00060I-Ns; Thu, 03 Nov 2016 14:55:02 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1c2ME9-00035P-DL for categories-list@mlist.mta.ca; Thu, 03 Nov 2016 14:55:01 -0300 In-Reply-To: <581B0EB3.4030304@cs.bham.ac.uk> Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9008 Archived-At: On 2016-11-03 12:17, Steve Vickers wrote: > Actually, maths is _strong_ on types. Yes, and I would say mathematics in particular as used within theoretical computer science (my chair is in that area), and how it focuses on types and type constructors, but the > ... way "HoTTematics" doesn't comply with mathematics. to me is a concern, e.g., since 'type constructors' are brought in from the outside, so as to say, and this is a bit of that "doesn't comply", isn't it, Steve? We've tried out something to keep those constructors "inside", not (yet) for that empty type, but some small pieces can be found following the links under GLIOC. It shows e.g. how we try to relate things back to Sch??nfinkel, Church and Curry and their G??ttingen times. Church's 'o' type in his 1940 paper is still not well understood, I think. His 'iota' is Martin-L??f's 'type', and we know how things went wrong when they started to say "type is a type". It was fixed but that fixing indeed "doesn't comply", does it? Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]