18 Dec
2002
18 Dec
'02
9:15 a.m.
On 16 Dec 2002, Andrej Bauer wrote:
I think I can answer my own question: it's enough to have conjunction, truth, and equations to get a complete semantics of lex categories. This really is just an exercise in categorical logic. Sorry for bothering everyone with it.
[CUT]
I think this does the job. Andrej
No, it doesn't: you need to include *some* existential quantification. In the syntax Andrej proposes, it's impossible to formulate the theory of categories (for the reason why this theory is a good test case, see Example D2.4.7 in "Sketches of an Elephant"). Peter Johnstone 18-Dec-2002 12:22:16 -0400,2720;000000000001-00000000