I've been trying to do some forcing arguments in intuitionistic ZF using Heyting valued models where the Heyting algebra I'm using is actually a bi-Heyting algebra (both a Heyting algebra and a co-Heyting algebra) and I've found that some interesting questions arise if I use the co-Heyting negations as well as/instead of the Heyting negation. I'm just wondering if anyone knows if any work has been done in constructing some kind of co-Heyting valued models of any kind of set theory? I guess such a theory would have to be paraconsistent. If this hasn't been done, could anybody give me some info/references about the current situation with respect to paraconsistent set theory and its model theory. Is there a dominant axiomatization?