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/ ]