From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3510 Path: news.gmane.org!not-for-mail From: Tom Hirschowitz Newsgroups: gmane.science.mathematics.categories Subject: intensional higher-order logic Date: Fri, 8 Dec 2006 16:11:48 +0100 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019349 9057 80.91.229.2 (29 Apr 2009 15:35:49 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:35:49 +0000 (UTC) To: cat-dist@mta.ca Original-X-From: rrosebru@mta.ca Fri Dec 8 19:22:41 2006 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Fri, 08 Dec 2006 19:22:41 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Gsoz4-0002gY-FW for categories-list@mta.ca; Fri, 08 Dec 2006 19:18:26 -0400 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 11 Original-Lines: 41 Xref: news.gmane.org gmane.science.mathematics.categories:3510 Archived-At: Dear all, Here is a probably easy question on categorical logic. If I understood correctly from Bart Jacobs' book [1], a topos, besides its elementary definitions, e.g., as a complete CCC with a subobject classifier, may be defined as a category whose subobject fibration is a higher-order fibration. Such subobject higher-order fibrations always have extensional entailment, in the sense that logical equivalence implies internal equality (which in HOL is necessarily Leibniz equality modulo iso). My question is twofold: (a) Is there an intensional equivalent to the notion of topos? In other words, is there a widely accepted categorical, elementary characterization of HOL? (b) If so, for these HOL categories, is there an analogue of the definition in terms of subobject fibrations? For instance, is it the case that for such HOL categories, e.g., the fibration of monos (or the codomain fibration) is a higher-order fibration? The question might be equivalent to: is there a well-established pair of a fibred construction F and an elementary doctrine D, such that for all category C, C is in D iff F (C) is a HO fibration? However, I am highly unsure that this formulation makes sense. Thanks and all that, Tom [1] B. Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999.