# Presheaves and Heyting Valued Models

I'm doing some reading on the relationship between the topos of pre-sheaves over a poset P, the topos of sheaves over the Heyting algebra H of sieves on P, and the Heyting valued model of intuitionistic ZF generated by H, and have come across some definitions that I find quite confusing. In particular, in these two papers,

Just to be clear: it's probably not presheaves over a (complete) Heyting algebra $H$ that you're interested in here, but rather sheaves over $H$. Cf. theorem 2.4.1 in your first link (page 506). The equivalence between sheaves over $H$ and the topos of $H$-valued sets (akin to Boolean-valued models of set theory), which is not obvious, was first established by Higgs in unpublished notes. I think a proof can be found in