Re: Famous unsolved problems in ordinary category theory

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Dear Rafael,

here is a list of problems from categorical logic that I find difficult
to solve and don't know the answer yet. Certainly they are more on the logical
side but categories are involved in all of them. I don't claim that these
problems are generally important for category theory but they simply do bother
me. I write this mail to show that there are technically hard problems and
with the salient hope that someone may come up with an answer. Nevertheless
I am aware that the subsequent list of problems might easly get a prize for
the "best collection of most misleading problems".

(1) In their booklet "Algebraic Set Theory" Joyal and Moerdijk defined
    for every strongly inaccessible cardinal \kappa a class of
    \kappa-small maps inside the effective topos.

    Does there exist a "generic" \kappa-small map such that all other maps
    can be obtained as pullbacks from this generic one?

    In their book the authors show the existence of a weakly generic one
    but this doesn't imply the existence of a generic one and I suspect
    there is none.

(2) Does there exist a model for Martin-L\"of's Intensional Type Theory
    which validates Church's Thesis?

    This question is due to M.Maietti and G.Sambin. Notice that type theory
    validates the axiom of choice and, accordingly, the statement is much
    stronger than saying that for every function from N to N there exists a
    code for an algorithm computing this function.

(3) In my habilitation thesis
    (www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf)
    I showed that the sconing of the effective topos (i.e. glueing
    Gamma : Eff -> Set) gives rise to a model of INTENSIONAL Martin-Loef
    type theory faithfully reflecting most of the weakness compared to
    EXTENSIONAL type theory.
    Martin Hofmann and I showed that the groupoid model refutes
    the principle UIP saying that all elements of identity types are equal.
    This has recently generalised to \omega-groupoids by M.Warren and there
    is recently some activity of constructing models based on abstract
    homotopy.

    Can one construct a categorical model model serving both purposes?

    This is an issue since the groupoid model and related ones constructed
    more recently have the defect that all types over N are fairly extensional
    and thus don't do the job which sconing of the effective topos does.

(4) Is the realizability model for the polymorphic lambda calculus
    parametric in the sense of Reynolds?
    It needn't be realizability over natural numbers.
    Would be interesting already for some pca!

Thomas



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]