# 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,

http://www.google.co.uk/url?sa=t&rct=j&q=heyting%20valued%20model%20topos%20of%20presheaves&source=web&cd=5&ved=0CEsQFjAE&url=http%3A%2F%2Fwww.ems-ph.org%2Fjournals%2Fshow_pdf.php%3Fissn%3D0034-5318%26vol%3D23%26iss%3D3%26rank%3D5&ei=goZmUqL1M6jX0QWWgIGwDQ&usg=AFQjCNFpEXFZRCmYhON_ZC1EMTZlYS0Lcw&bvm=bv.55123115,d.d2k

http://www.google.co.uk/url?sa=t&rct=j&q=sheaves%20and%20logic&source=web&cd=1&cad=rja&ved=0CCwQFjAA&url=http%3A%2F%2Flink.springer.com%2Fchapter%2F10.1007%252FBFb0061824&ei=141mUsi-A-KS0AX4gYHYCw&usg=AFQjCNHIVjsvii1zx0O6h-5osTktPAxb_Q&bvm=bv.55123115,d.d2k

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.

## 1 Answer

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

• Fourman, M.P. and D.S. Scott (1979). Sheaves and logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott (Eds.), Applications of Sheaves, Proceedings, Durham 1977, Volume 753 of Lecture Notes in Mathematics, pp. 302-401. Springer-Verlag, Berlin.

For a more modern understanding of that theorem, a useful keyword is 'tripos'. TRIPOS = Topos Representing Indexed Partially Ordered Set is a notion introduced (by some combination of Hyland, Johnstone, and Pitts) to unify toposes of sheaves over complete Heyting algebras and realizability toposes coming from partial combinatory algebras. Some pointers that might be useful to you are the nLab article on tripos, and a survey article by Pitts, Tripos theory in retrospect (pdf).