CCCs of Stable Domains

To: types@theory.LCS.MIT.EDU
Subject: CCCs of Stable Domains
From: Paul Taylor <pt%doc.imperial.ac.uk@nss.cs.ucl.ac.uk>
Date: Wed, 25 Jan 89 10:54:13 EST
Sender: meyer@theory.LCS.MIT.EDU
Date: Tue, 24 Jan 89 18:52:57 GMT
To: types@theory.LCS.MIT.EDU

			The Trace Factorisation
			 and Cartesian Closure
			 for Stable Categories

In August I advertised on "types" that I had proved that the following
2-category is cartesian closed:
   objects:  locally small categories with small filtered colimits
	and a set of objects of which from which any object can be
	constructed using filtered colimits, such that every slice
	category [is a continuous category in the sense of Johnstone-Joyal]
	[is complete, and filtered colimits are preserved by pullbacks].
   morphisms: functors preserving filtered colimits, which on every
	slice have left adjoints
   2-cells: cartesian natural transformations
This is a substantially larger 2-category than those studied by Berry,
Girard, Coquand-Gunter-Winskel, Coquand, myself and Lamarche.

Several people requested copies of my work then; I confess I have a
bad reputation for supplying copies, but
I HAVE NOW COMPLETED (ALMOST ALL OF) THE PROOF AND AM MAKING COPIES
FOR DISTRIBUTION THIS EVENING.

The paper begins with a discussion of diagonal universality, which
generalises the well-known idea of a "universal map from an object
to a functor" (one of the ways of saying the functor has a left
adjoint). This is developed into the trace factorisation, and it
is shown that many examples from Girard and Diers fit into this
picture. After proving relative cartesian closure (including dependent
sums and products) for the largest 2-category possible, the paper
ends with a systematic survey of cartesian closed subcategories,
including all of those discussed by other authors.

My paper, which will probably not be published in its present extended
form (70 pages) touches on a wide range of issues, not all of them
directly connected with cartesian closure. To give you an idea, here is
the list of definitions:

approximation			meet-continuity
Beck condition			minimal upper bound (mub)
bifibration			mlex-category
cartesian (nat) transformation	multijoin	
coalgebra			op-fibration, op-horizontal
coherence space			ordinals
comonad				orthogonal arguments
comparison			plex-category
comultiplication		polycolimit candidates
coseparator			power series		
dI-domains			profinite
dependent sum & product		projection
diagonal universality		pullback-continuous
dilators			pullbacks
directed joins			qualitative domain
discrete fibration		quantitative domain
discretely stable functor	rigid bifibration
equivalence relation		rigid comparison
event structure			Scott-continuous functor
factorisation system		Scott-trace
fibration			semigranular categories
filtered colimits		size
finitely presentable		slices, class of
first order polymorphism	solution set condition
free group			spectrum
Gabriel-Ulmer duality		spins, class of
Galois group			split extension & fibration
Girard-Reynolds polymorphism	spread
Giraud's theorem		stable functor
Grothendieck fibration		stable order
group extension			stably stable functor
groupoid			strongly finite
homomorphism			strongly presentable
horizontal lifting		structure
injections			toposes
input patterns			total category
involution			trace
isomorphic			unit
isotomy				universal map
lifting of the map		vertical
lifting of the triangle		weakly equivalent
limit-colimit coincidence	well-powered	
linear order			wide pullback
locally cartesian closed	Zariski spectrum
locally finitely (multi-, poly-)presentable			

Anyone who would like a copy of this paper should email me their
postal address. I promise to dispatch quickly.

Paul Taylor,  Department of Computing, Imperial College,
180 Queen's Gate, London SW7 2BZ, UK.
+44 1 589 5111 x 4981