Hello, I have started reading the stuff on internal language in McLarty's book and also in the Lambek/Scott book. I am trying to short circuit my learning a little (in a vast and humbling subject!) What are the models for topos logic? The class of Heyting algebras? Regards, Bill