Dear categorists, A standard method for doing logic in category theory is, as far I as know, by imposing more and more conditions on the subobject posets Sub(X), which are equivalence classes of monomorphisms with X as the codomain. By adding more and more assumptions of this kind one gets more and more powerful internal logics. The connection between predicates and functions does not arise in all these stages as long as one does not request existence of the subobject classifier (therefore almost certainly turning the whole thing into a topos). What I am wondering about is whether an alternative approach have ever been developed, namely by postulating an internal truth-value object Omega, by introducing predicates as exponentials Omega^X, and so forth. I would expect, if such an idea have ever been developed it would yield one of the many ways to provide foundations to the topos theory. The fact that is not well-known sort of indicates that it is probably not such a robust idea, in which case I would be grateful if someone would explain me why. The only approach to topos theory I know, which might be relevant here is the one by allegories. Starting from a category C with a distinguished object Omega (say, internal Heyting algebra) we can introduce an allegory having the same object as C and as morphisms A->B those of C having form A x B -> Omega. Antiinvolution would then follow by swapping the arguments, and the intersection can be made deducible from the axiomatic structure of Omega. The question is, of course, the modular law, and the conditions under which it would follow. Has anyone studied that? I would be very grateful for any hints and/or references on the subject. Best regards, -- Sergey Goncharov, Assistant Professor FAU Erlangen-N?rnberg Phone: +49-91-3185-64031 Chair for TCS Fax: +49-91-3185-64055 Wetterkreuz 13 Email: Sergey.Goncharov@cs.fau.de D-91058 Erlangen Web: http://www8.cs.fau.de/~sergey [For admin and other information see: http://www.mta.ca/~cat-dist/ ]