Re: cleavages and choice

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Dear Jean,

It has not been my intention to defend indexed categories against
fibered categories. I just wanted to say that it is sometimes
"convenient" to use cleavages.

First of all I would say that fibrations with cleavages are not the
same as indexed categories. Firstly, because the coherence conditions
for the maps chosen by the cleavage are determined by the functor and
do not have to be stated explicitly. Secondly, for fibrations with
cleavages one can show that they are closed under composition which
for indexed categories would be (close to) impossible.

Nevertheless, I agree with you that it is in general preferable to
formulate things in such a way that one avoids reference to cleavages
as far as possible. Sometimes, however, this makes things a bit more
complicated as I want to illustrate by the following example.

Chevalley's original formulation of his famous condition for internal
sums is much more convenient than the one usually found in the literature.
An analogue can be formulated for internal products (as in section 7
of my Notes on Fibrations you have mentioned). In Th.7.1 of loc.cit. I
have given a characterization of fibration having internal products which
avoids any reference to cleavages. This appears to me a bit clumsy and
there is a version using cleavages which essentially says that reindexing
functors have right adjoints and that their counits are preserved by
reindexing up to isomorphism. This latter version is useful when
checking that a given fibration has internal products as is necessary e.g.
when constructing models of type theory.

But in any case I think that conceptually it is preferable to define P
having internal products as P^op having internal sums. This formulation
is free from cleavages but for using it in concrete instances it is
sometimes useful to have equivalent formulations available which don't
abhor making reference to reindexing functors and thus to cleavages.

But this is a pragmatic issue and not a foundational issue. The same applies
to linear algebra. If it is convenient to refer to bases of vector spaces
I am not against doing so. But, of course, it would be stupid to require
all vector spaces to be endowed with bases.

For this reason I want to CORRECT the point of view of my previous mail.
One should not require all fibrations to be endowed with a cleavage. Rather
one should be open to accept some strong choice principles on the meta level
which allow one to assume the existence of cleavages whenever convenient.
But, definitely, one should give most definitions and constructions in a way
not referring to cleavages.

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]