[Prev][Next][Index][Thread]
CCCs of Stable Domains
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