> He observes that these two ideas fit together in Krivine-style realizability models of classical logic: every formula can be interpreted as a set of proofs an

> He observes that these two ideas fit together in Krivine-style realizability models of classical logic: every formula can be interpreted as a set of proofs and refutations, and the interaction of a proof with a refutation yields a behaviour in the answer type. I've wanted to see this paradigm implemented in the Isbell envelope of a category, whose objects are pairs of a presheaf and copresheaf T, E and a natural transformation from T(-) x E(--) ~> Hom(-,--) . I think it would be really striking if the answer type could be Hom itself, which I like to think of as a formalisation of the turnstile |- by itself.