From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4929 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Famous unsolved problems in ordinary category theory Date: Fri, 5 Jun 2009 16:17:01 +0200 Message-ID: Reply-To: Thomas Streicher NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1244224326 13348 80.91.229.12 (5 Jun 2009 17:52:06 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 5 Jun 2009 17:52:06 +0000 (UTC) To: Hasse Riemann , categories@mta.ca Original-X-From: categories@mta.ca Fri Jun 05 19:52:03 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1MCdaF-0001x5-8M for gsmc-categories@m.gmane.org; Fri, 05 Jun 2009 19:52:03 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1MCcwV-0000SF-4y for categories-list@mta.ca; Fri, 05 Jun 2009 14:10:59 -0300 Content-Disposition: inline Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:4929 Archived-At: 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/ ]