locally cartesian closed categories

[Paul Taylor <pt07@PaulTaylor.EU>]

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