Dear Dale, I don't know if it appeared anywhere earlier, but the result for an arbitrary poset is Proposition 8.4 in Birkedal, Mogelberg, Schwinghammer and Stovring's paper "First steps in synthetic domain theory: step-indexing in the topos of trees". http://www.cs.au.dk/~birke/papers/sgdt-journal.pdf Paul On 12/11/14 18:46, Garraway, Dale wrote:
Hi All
Could some one please send me a reference of the fact that the category of presheaves on a Heyting algebra $H$ is equivalent to the category of sheaves on the Heyting algebra of down closed subsets of $H$. I believe this is true in general for any partial order so a reference to either would be greatly appreciated.
Dale Garraway Dept. of Math, Eastern Washington dgarraway@ewu.edu
-- Paul Blain Levy School of Computer Science, University of Birmingham http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]