We know that the category of Boolean algebras and homomorphisms is the ind-completion of $\mathsf{FinBA}$, the full subcategory of $\mathsf{BA}$ of finite Boolean algebras. I am wondering if the same holds for the category $\mathsf{HA}$ of Heyting algebras and Heyting morphisms.
Since Heyting algebras are models of an algebraic theory we know that it has filtered colimits. But I don't know how to prove that every Heyting algebra is the colimit of the diagram of its finite subalgebras.
It's not true that every Heyting algebra is the filtered colimit of its finite subalgebras. Very generally, a finitary algebraic structure is the filtered colimit of its finite substructures iff every finitely generated substructure is finite. But not every finitely generated Heyting algebra is finite (in fact, even a Heyting algebra generated by just one element can be infinite; here is a picture of the free Heyting algebra on one generator).
The ind-completion of the category of finite Heyting algebras is the category of "locally finite" Heyting algebras, the Heyting algebras for which every finitely generated subalgebra is finite.