  Any refinement system (= functor) has a fully faithful representation in the
refinement system of presheaves, by interpreting types as relative slice
categories, and refinement types as presheaves over those categories. Motivated
by an analogy between side effects in programming and *context effects* in
linear logic, we study logical aspects of this "positive" (covariant)
representation, as well as of an associated "negative" (contravariant)
representation. We establish several preservation properties for these
representations, including a generalization of Day's embedding theorem for
monoidal closed categories. Then we establish that the positive and negative
representations satisfy an Isbell-style duality. As corollaries, we derive two
different formulas for the positive representation of a pushforward (inspired
by the classical negative translations of proof theory), which express it
either as the dual of a pullback of a dual, or as the double dual of a
pushforward. Besides explaining how these constructions on refinement systems
generalize familiar category-theoretic ones (by viewing categories as special
refinement systems), our main running examples involve representations of Hoare
Logic and linear sequent calculus.
