From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9043 Path: news.gmane.org!.POSTED!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Predicativity in Categories Date: Thu, 1 Dec 2016 15:55:10 +0100 Message-ID: References: Reply-To: Thomas Streicher NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: blaine.gmane.org 1480617685 14453 195.159.176.226 (1 Dec 2016 18:41:25 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Thu, 1 Dec 2016 18:41:25 +0000 (UTC) Cc: categories@mta.ca To: Sergey Goncharov Original-X-From: majordomo@mlist.mta.ca Thu Dec 01 19:41:21 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 1cCWIK-0002sN-TU for gsmc-categories@m.gmane.org; Thu, 01 Dec 2016 19:41:21 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:46599) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1cCWHc-00088v-NW; Thu, 01 Dec 2016 14:40:36 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1cCWHd-00029Q-Pv for categories-list@mlist.mta.ca; Thu, 01 Dec 2016 14:40:37 -0400 Content-Disposition: inline Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9043 Archived-At: Categorical Logic is such a versatile tool that it allows to give an account uf both impredicative and predicatives systems. A topos is a categorical account to higher order logic and thus impredicative. A logos (Freyd) gives an account of intuit. first order logic and thus is "predicative". A locally cartesian closed category (after splitting) is a model of Martin-Loef type theory. That is predicative. Both predicative and impredicative universes can be defined categorically within lcc's. This was done is the second half of the 1980s by many people (including myself). Whether category theory itself is "impredicative" however is an ill-posed question in my eyes. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]