Usefulness of coherence in coherence spaces-based interpretations of type systems I'm going through "Proofs and Types", and I'm trying to internalize the notion of coherence spaces. In particular, I'm trying to understand what additional information is given by the fact that two tokens $\alpha_1, \alpha_2$ of a coherence space $\mathcal{A}$ are, well, coherent. Sure, that means that there exists a point of $\mathcal{A}$ such that both tokens belong to it (in particular, $\\{ \alpha_1, \alpha_2 \\}$ will do). But what does it give us if we are to analyze and interpret a particular type system? The only use of the notion of coherence I've seen so far is basically in prove certain tokens of "composite" (product or arrow) coherent spaces are coherent.

You might find this article useful.

To distill what it says down a bit, tokens represent individual pieces of information you can have about a value of the type. Tokens are coherent if there is a value of the type about which it would make sense to learn both pieces of information (i.e. they are actually "coherent" pieces of information).

So in the $\mathsf{Bool} × \mathsf{Bool}$ example from the article, the pieces of information are:

1. The first part of the pair is $\mathsf{false}$
2. The first part of the pair is $\mathsf{true}$
3. The second part of the pair is $\mathsf{false}$
4. The second part of the pair is $\mathsf{true}$



1 is coherent with 3 and 4, because $(\mathsf{false},\mathsf{true})$ and $(\mathsf{false},\mathsf{false})$ are values. 1 is not coherent with 2 because it's impossible for the first part of the pair to be _both_ $\mathsf{true}$ and $\mathsf{false}$.