Further to Peter's remark that the opposite of the category finitely presented Heyting algebras is rather nice ... one particular sense in which it is nice is that it is a lextensive category! So -- to seemingly contradict Peter :-) -- it does have a partial map classifier (but of course not for all monics)! The fact that it is a lextensive category can be obtained, by checking some Heyting algebra identities, from "Conditional Control is not quite Categorical Control" IV Higher Order Workshop, Banff 1990, Workshops in Computing (Springer-Verlag) 190-217 (1991) where the general question of when the opposite of an algebraic theory is extensive is answered. Any extensive category can be fully and faithfully embedded in a topos so as to preserve sums and limits ... so the ability to embed the opposite of Heyting algebra "nicely" into a topos can also be read from these results. -robin P.S.Whether this embedding has the other logical properties mentioned is, of course, another question ... On 12 Feb, Prof. Peter Johnstone wrote:
On Tue, 11 Feb 2003, Galchin Vasili wrote:
I have some questions about the category whose objects are Heyting algebras and whose arrows are Heyting algebra homomorphims.
The category of Heyting algebras has no hope of being cartesian closed because its initial object (the free HA on one generator) is not strict initial. It doesn't have a subobject classifier either, because the theory of Heyting algebras doesn't have enough unary operations to satisfy the conditions of Theorem 1.3 in my paper "Collapsed Toposes and Cartesian Closed Varieties" (J. Algebra 129, 1990).
On the other hand, the terminal object in the category of Heyting algebras is strict, which suggests that the dual of the category might come rather closer to being a topos (although, by an observation which I posted a couple of months ago, it can't have a subobject classifier). Indeed, the dual of (finitely-presented Heyting algebras) is remarkably well-behaved, as shown by Silvio Ghilardi and Marek Zawadowski ("A Sheaf Representation and Duality for Finitely Presented Heyting Algebras", J.Symbolic Logic 60, 1995): they identified a particular topos in which it embeds (non-fully, but conservatively) as a subcategory closed under finite limits, images and universal quantification.
Peter Johnstone