We explore a novel variant of logical relations that maps types not
merely to partial equivalence relations on values as is commonly done,
but rather to a proof-relevant generalisation thereof, namely setoids.

The objects of a setoid establish that values inhabit semantic types,
whilst its morphisms are understood as proofs of semantic equivalence.

The transition to proof-relevance allows one to remedy the notorious
problems brought about by the use of existential quantification in
Kripke logical relations, namely failure of admissibility and spurious
functional dependencies.

We illustrate the novel format with two applications: a direct-style
validation of Pitts and Stark's equivalences for ``new'' and a
denotational semantics for a region-based effect system that supports
type abstraction in the sense that only externally visible effects
need to be tracked; non-observable internal modifications, such as the
reorganisation of a search tree or lazy initialisation, can count as
`pure' or `read only'. This `fictional purity' allows clients of a
module soundly to validate more effect-based program equivalences than
would be possible with traditional effect systems.