I seem to remember that some years ago at MFPS conference in Pittsburgh, Peter Freyd gave a talk on the internal logic of lex categories. Is this correct, and if so, has it been written down? It's probably easy to explain the gist of the talk, so if it has not been written down, perhaps someone with a memory better than mine can tell us what Freyd said. (Insert remarks about horse's mouth here.) Here is an attempt at reconstructing the logic. We want a logic that can be interpreted in any category C with finite limits, and we want a suitable completeness theorem, i.e., the semantics in lex categories is complete. Since C has pullbacks, Sub(A) has finite limits for any A. This means we should have the logical constant truth T and conjunction: T phi and psi Since there are equalizers in C, we should also allow equality (at each type A): t =_A u So now the question is what else is needed. We're not done yet since, semantically speaking, we have axiomatized equalizers and only pullbacks of monos along monos. Presumably we have to axiomatize the terminal object: 1 type ("1 is a type") * : 1 ("* is an element of 1") t =_1 * ("every element of 1 is equal to *") This still isn't enough because we don't have general pullbacks, or is it? I suspect we need not worry about binary products because the syntactic model will have them "for free". What did Peter Freyd say about this? Andrej Bauer Deptatment of Mathematics and Physics University of Ljubljana Slovenia http://andrej.com/ 16-Dec-2002 17:26:10 -0400,1208;000000000001-00000000