Dialectica space

Dialectica spaces are a categorical way of constructing models of linear logic.
They were introduced by Valeria de Paiva, Martin Hyland's student, in her doctoral thesis, as a way of modeling both linear logic and Gödel's dialectica interpretation—hence the name.
Given a category "C" and a specific object "K" of "C" with certain (logical) properties, one can construct the category of Dialectica spaces over "C", whose objects are pairs of objects of "C", related by a "C"-morphism into the given object. Morphisms of Dialectica spaces are similar to Chu space morphisms, but instead of an equality condition, they have an inequality condition, which is read as a logical implication, the first object implies the second.