morphisms between (particular) hyperdoctrines

morphisms between (particular) hyperdoctrines

[Thomas Streicher]

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