This question concerns Bart Jacobs' paper "Simply typed and untyped Lambda Calculus revisited", in "Applications of Categories in Computer Science", Durham Proceedings, London Mathematical Society Lecture Note Series No. 177 In Example 3.2, Bart Jacobs constructs a term model for a certain kind of fibration (or indexed category). The base category has contexts as objects, i.e., finite tuples of type declarations, while morphisms are finite tuples of (beta-eta-equivalence classes of) terms. I have some trouble seeing that this category has finite products, given by concatenation of contexts, as claimed. Unless each variable can only be used once, isn't it possible to overwrite a declaration x:tau by x:sigma in a different context? This seems to make concatenation nonsymmetric (and one loses the projections as well). Computer Scientists here tell me that the ability to overwrite type declarations is essential for their work. I don't know whether Bart Jacobs has access to the net; maybe someone can forward this question to him? Thank you. regards, J"urgen -- J"urgen Koslowski | If I don't see you no more in this world Department of Mathematics | I meet you in the next world Kansas State University | and don't be late! koslowj@math.ksu.edu | Jimi Hendrix (Voodoo Chile) ==============================================================================