nLab
HeytAlg

$\mathrm{Heyt}\mathrm{Alg}$ is the category whose objects are Heyting algebras and whose morphisms are Heyting algebra homomorphisms, that is lattice homomorphisms which also preserve the Heyting implication. $\mathrm{Heyt}\mathrm{Alg}$ is a subcategory of Pos.

$\mathrm{Hety}\mathrm{Alg}$ is given by a finitary variety of algebras, or equivalently by a Lawvere theory, so it has all the usual properties of such categories. By general abstract nonsense, the free Heyting algebra on a set $X$ exists, but it is not easy to describe in general.

• The free Heyting algebra on the empty set is the Boolean domain $\{\perp ,\top \}$.
• The free Heyting algebra on a singleton $\{x\}$ is infinite, although it has a nice picture.

category: category