Michael Makkai has shown that something called the Craig Interpolation lemma is equivalent to fact that in Heyting algebras a pushout of an injection is an injection.

To be precise I think Michael was claiming a new proof of the latter fact (the equivalence of CI to pushout stability is well known, to some).

Now it is easy to show that a pushout of an injection with a quotient map is an injection, so the question is reduced to the amalgamation property. Anyone have an easy proof of that?

For a constructive (and easy!) proof see my paper "Amalgamation and interpolation in the category of Heyting algebras", Jour Pure Appl. Algebra 29(1983)155--165. Andy Pitts ======================================