Re: Category of Heyting Algebras

[Robin Cockett <robin@cpsc.ucalgary.ca>]

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
>
>
>
>