On 16 Dec 2002, Andrej Bauer wrote:
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.)
Someone ought to contribute the name of Michel Coste to this discussion, since he produced a perfectly serviceable syntax for cartesian logic over twenty years before Peter Freyd, and ten years before Colin McLarty. His version was published in SLNM 753 (the proceedings of the 1977 Durham Symposium on Applications of Sheaves). Peter Johnstone 17-Dec-2002 19:04:31 -0400,906;000000000001-00000000