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,
presheaves over a Heyting algebra are defined in a way that I have never seen before. I can't seem to manage to reconcile the definitions used in these papers with the modern standard definition (contravariant set-valued functor). Could anyone either explain to me why the definitions are equivalent, or point me in the direction of a good reference? Thanks.