Re: locally cartesian closed categories

Re: locally cartesian closed categories

[Eduardo Dubuc]

hi,

yet another point in favor that terminal object and products  should not
be mandatory in locally cartesian closed categories:

terminal (or products) implies connection, fiber products don't.

compare with the notion of cofilter category (axiom similar to existence
of products), is connected, while pseudofiltered (axiom similar to
existence of fiber products), is not connected.

this is essentially the difference between filterness and cofilterness,
with all what it means

same thing, fiber products and not products are in the essence of the
notion of locally cartesian closedness

ps: congratulations to Bob R., I fully agree with all the good things that
were said recently about his handling of this list (not an easy job !).

eduardo dubuc

Re: locally cartesian closed categories

[Lutz Schroeder]

> I agree with Jean Benabou, Fred Linton and Vaughan Pratt that the
> definition of a locally cartesian closed category should NOT require
> a terminal object.   

[...]

> I confess that I'm a bit surprised to find that the consensus agrees
> with me, so to set matters straight I should also point out that my
> argument applies equally to elementary toposes and other familiar
> structures of categorical logic.

Such as cartesian closed categories, for instance. I would like to take
the opportunity to point to my paper "Life without the terminal type" in
CSL 2001, where I prove that every "almost" cartesian category, i.e. one
without a terminal object, extends uniquely to a cartesian closed
category with terminal object. There is also a similar result for
toposes; the wording is not quite as straightforward as for cartesian
closed categories, as one has to formulate (say) the definition of a
subobject classifier without reference to a global element True. I
recall having thought about locally cartesian closed categories as well,
but I do not think I really got anywhere (and actually I just see
there's a remark in the paper that says as much).

Lutz Schröder

-- 
------------------------------------------------------------------
PD Dr. Lutz Schröder                  office @ Universität Bremen:
Senior Researcher                     Cartesium 2.051
Safe and Secure Cognitive Systems     Enrique-Schmidt-Str. 5
DFKI-Lab Bremen                       FB3 Mathematik - Informatik
Robert-Hooke-Str. 5                   Universität Bremen
D-28359 Bremen                        P.O. Box 330 440
                                      D-28334 Bremen
phone: (+49) 421-218-64216            Fax:   (+49) 421-218-9864216
mail: Lutz.Schroeder@dfki,de
www.dfki.de/sks/staff/lschrode
------------------------------------------------------------------


-------------------------------------------------------------
Deutsches Forschungszentrum für Künstliche Intelligenz GmbH
Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern

Geschäftsführung:
Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender)
Dr. Walter Olthoff

Vorsitzender des Aufsichtsrats:
Prof. Dr. h.c. Hans A. Aukes

Amtsgericht Kaiserslautern, HRB 2313
-------------------------------------------------------------

locally cartesian closed categories

[Paul Taylor]

I agree with Jean Benabou, Fred Linton and Vaughan Pratt that the
definition of a locally cartesian closed category should NOT require
a terminal object.   I expressed this view in a footnote on page 499
of "Practical Foundations of Mathematics", with a justification
similar to Vaughan's.

The simplest formulation is that an LCCC is a category every slice of
which is a CCC.  In particular, every slice has binary products,
which are pullbacks in the whole category.

Objects of an LCCC and the slices that they define correspond to
objects of a base category and the fibres over them in a fibred or
indexed formulation of logic, and to contexts in a syntactical one.

Contexts are collections of hypotheses.  The terminal object or
empty context is the one with no hypotheses at all. However, as
the 18th century logician Johann Lambert remarked, ``no two concepts
are so completely dissimilar that they do not have a common part''.

If "naturally occurring" LCCCs usually have terminal objects,
I suggest that that may be because they are already slices of
some more general picture.

For more or less the same reason, we never actually concatenate
two contexts, but build them up one hypothesis at a time.  So I would
say that, whilst an LCCC has pullbacks, it need not have binary
products.   (My footnote refers to "other authors" who said that
LCCCs should have binary products;  I think I may have had Thomas
Streicher in mind, but I don't recall what he may have said
or in what paper.)

I confess that I'm a bit surprised to find that the consensus agrees
with me, so to set matters straight I should also point out that my
argument applies equally to elementary toposes and other familiar
structures of categorical logic.

----

While we're playing around with the structures of categorical logic,
let me try another related question.

Any topos is a CCC with an internal Heyting algebra.

[WARNING TO STUDENTS: whilst this statement is true, it's NOT
(equivalent to) the correct definition.]

I am sorry to say that I have seen papers emanating from respectable
universities in which the authors have appeared to believe that this
is the definition.   (One of the papers that I have in mind cites
many eminent categorists, who may perhaps have an opinion about having
their names appear alongside a lot of complete nonsense.)

But I wonder whether anyone has taken this idea seriously, and
investigated how much logic such a category would admit?

The version of this question that particularly interests me is this:

Suppose that the category has all FINITE LIMITS (terminal object,
finite products and equalisers) and POWERS  Sigma^X of an internal
DISTRIBUTIVE LATTICE (Sigma, top, bot, meet, join).   Maybe there
is also a natural numbers object N and joins Sigma^N->Sigma with
the Frobenius law.  (I would also like this to obey the monadic
and Phoa principles of ASD, but I'm not going to spell them out here.)

Maps X->Sigma give rise to a "geometric logic" of "open" subspaces.

Then the order relation between maps X->Sigma^Y leads to a richer
logic of "general" subspaces,  with  =>  and  forall_Y.

A logical formula of the more general form consists of geometric
sub-formulae joined together with  =>  and forall,  to which we might
add  the other first order connectives as "syntactic sugar", defined
in the usual classical way.   If a geometric sub-formula is immediately
enclosed in forall_K or exists_N, where K happens to be compact or
N overt, then this a priori more general quantifier may be considered
to be part of the geometric sub-formula.

Does this idea ring any bells?

Paul Taylor