I am reading (Taylor and translation of) Jean-Yves Girard's monograph _Proofs and Types_. Section 8.2 and following concern “coherence spaces”. I am having trouble connecting this with other things I know, and other sources haven't helped yet.
Girard presents two examples of coherence spaces: $\def\Bool{{\mathcal{Bool}}}\Bool$ and $\def\Int{{\mathcal{Int}}}\Int$, both of which are “flat”: none of the tokens are coherent. These are simple enough. He also presents an non-example of a coherence space. (p.55) And he says (8.2.2, p. 56) “the aim is to interpret a type by a cohrence space $\def\A{\mathcal A}\A$, and a term of this type by a point of $\A$”, by which he means a mututally-coherent set of tokens, sometimes elsewhere called a “clique”.
I am trying to make coherence spaces match up with types as I understand them already. The two flat coherence spaces Girard describes looks just like the corresponding Scott domains, with the empty clique $\varnothing$ playing the part of $\bot$. Similarly the unit type $\def\Unit{{\mathcal Unit}}\Unit$ with only one element is the coherence space whose web has a single vertex.
But at this point I start to get stuck.
I think what would help me most is a short account of the way that the coherence space concept would account for the following three types:
1. `data Wrapbool = V Bool`
2. `data Wrapunit = W Unit`
3. `data Pairbool = (Bool, Bool)`
`Wrapunit` ought to be flat, and identical to $\Unit$, except that in the conventional account, it has three elements ($W (), W\Bot, \Bot$) where $\Unit$ has only two ($(), \Bot$). Are `Wrapunit` and $\Unit$ the same when considered as coherence spaces, or different? And if different, what is the difference?
Similarly `Wrapbool` has four elements where $\Bool$ has only three.
In `Pairbool`, how many tokens are in the web? Four? Like this?
$$\begin{array}{ccc}
TF & — & TT \\
\lvert & & \rvert \\
FF & — & FT
\end{array}$$
which yields a coherence space with 9 cliques (four with two elements, four singletones, and $\varnothing$).
In section 8.4 Girard defines a direct product of coherence spaces, but it doesn't look like the direct product I need to get a product type; it looks more like a union type. If the coherence space for `Pairbool` is the square of the coherence space for $\Bool$, how? It has 4 2-cliques, but if those are the total elements of $\Bool^2$, then what are do the 1-cliques mean?
I have tried reading:
1. [Can you explain an intuition behind Coherent Spaces?](https://cstheory.stackexchange.com/questions/34203/can-you-explain-an-intuition-behind-coherent-spaces)
2. [Wikipedia](https://en.wikipedia.org/wiki/Coherent_space)
3. [Linear logic wiki](http://llwiki.ens-lyon.fr/mediawiki/index.php/Coherent_semantics)
I've also tried to read ahead in _Proofs and Types_, hoping that something later on will connect with what I already know, and then I will be able to work backward to understand what is going on, but I haven't been successful in this either.