Are there any free or cofree boolean algebras?

Question

A boolean algebra is an algebra with the binary operations $\wedge$, $\vee$, an unary operation $\neg$, and constants $0$, and $1$, satisfying axioms. A heyting algebra is an algebra with the binary operations $\wedge$, $\vee$, $\to$, and constants $0$ and $1$ satisfying axioms.

They both form the evident categories, being types of algebras. There is a functor from the category of boolean algebras to the category of heyting algebras, where $p \to q = \neg p \vee q$, and all other operations the same.

My question is, taking this as a forgetful functor, which heyting algebras have free or cofree boolean algebras. In general, is there a free or cofree functor from the category of heyting algebras to the category of boolean algebras.

Answer 1

As Zhen Lin said in the comments, there is a very general argument that answers your problem.

Denote $\omega$ for the category of finite ordinals with set-functions between them.

Definition 1. A Lawvere theory is a finite-product-preserving bijective-on-objects functor $\ell \colon \omega^\circ \to \mathcal T$.

A morphism $f$ from the Lawvere theory $\ell_1 \colon \omega^\circ \to \mathcal T_1$ to the Lawvere theory $\ell_2 \colon \omega^\circ \to \mathcal T_2$ is a finite-product-preserving functor $f \colon \mathcal T_1 \to \mathcal T_2$ such that $f \circ \ell_1 = \ell_2$.

Definition 2. A model for the Lawvere theory $\ell \colon \omega^\circ \to \mathcal T$ is a finite-product-preserving functor $\mathcal T \to \mathsf{Set}$. Together with natural transformations, models form a category $\operatorname{Mod}(\ell)$.

Now, if $f$ is a morphism from $\ell_1$ to $\ell_2$, one has a restriction functor from the models of $\ell_2$ to the models of $\ell_1$: $$ \operatorname{Mod}(\ell_2) \to \operatorname{Mod}(\ell_1), \quad M \mapsto M\circ f $$

Fact. Let $\mathcal A,B$ be small categories with finite products and $j \colon \mathcal A \to \mathcal B$ a functor between them. If $F \colon \mathcal A \to \mathsf{Set}$ is finite-product-preserving, then so is its left kan extension $j_!F \colon \mathcal B \to \mathsf{Set}$.

Hence, the restriction functor described above admits a left adjoint $$ \operatorname{Mod}(\ell_1) \to \operatorname{Mod}(\ell_2),\quad M \mapsto f_!M $$

---

If $\ell_1$ is the Lawvere theory of heyting algebras and $\ell_2$ the one of boolean algebras, there is a (inclusion) morphism $f \colon \ell_1 \to \ell_2$. The restriction functor is just the 'forgetful' functor you described. It then admits a left adjoint, meaning there is a free functor.

Edit. Also, see this section of the nLab page on Lawvere theories.