From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4092 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: morphisms between (particular) hyperdoctrines Date: Sat, 17 Nov 2007 14:35:28 +0100 (CET) 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 1241019715 11671 80.91.229.2 (29 Apr 2009 15:41:55 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:41:55 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Sat Nov 17 12:38:35 2007 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 17 Nov 2007 12:38:35 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1ItQS2-0002f5-KY for categories-list@mta.ca; Sat, 17 Nov 2007 12:23:22 -0400 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 46 Original-Lines: 45 Xref: news.gmane.org gmane.science.mathematics.categories:4092 Archived-At: Jean Benabou has asked whether morphisms between hyperdoctrines have been considered in categorical logic. In work on "parametric polymorphism" (for polymorphic lambda calculus), see Birkedal, Lars; Mogelberg, Rasmus E. Categorical models for Abadi and Plotkin's logic for parametricity. Math. Structures Comput. Sci. 15 (2005), no. 4, 709--772. based on previous work by Robinson and Rosolini (1994) on "Reflexive graphs and parametric polymorphism" (Proc. LICS 1994) reflexive graphs in the category of PL-hyperdoctrines (models for polymorphic lambda calculus) find an essential use. Moreover, the involved PL-hyperdoctrines live over different bases. In B.Jacobs book "Categorical Logic and Type Theory" (Elsevier, 1999) the work of Robinson and Rosolini is briefly addressed and a few hundred pages earlier he discusses morphisms between hyperdoctrines for equational logic (however, without further exploiting this notion). In work on "tripos theory" (late 70ies) Hyland, Johnstone and Pitts have considered geometric morphisms between triposes and shown that via the tripos-to-topos construction give rise to (localic) geometric morphisms between the associated toposes. This has been used over and over again in subsequent work on realizability and related structures (e.g. modified realizability). Currently a student of mine (Jonas Frey) is writing up in his diploma thesis a universal characterisation of the "tripos-to-topos" construction as an (appropriately lax) left adjoint to the functor sending a topos to its associated subobject fibration (which is a tripos). Even in order to formulate this result one has to consider a category of triposes over different bases. (I am confident that his work will be available from my homepage end of this year). As far as I know there is no systematic study of morphism between hyperdoctrines (of the kind as Jean probably has in mind). But now and then particular instances have been considered and put to use for particular purposes. Thomas Streicher