<p><strike>I now see how to define equalizers for coherence spaces, which means pullbacks always exist (since products do).</strike> I don't know how to do this, actually....</p>

<p>Recall that composition is the usual relational composition, so if $f : A \to B$ and $g : B \to C$, then: </p>

<p>$f ; g = \{(a,c) \in A \times C \;|\; \exists b \in B.\; (a,b) \in f \land (b,c) \in g\}$</p>

<p>(In this definition, the existential actually implies <em>unique</em> existence. Suppose that we have $b&#39; \in B$ such that $(a,b&#39;) \in f$ and $(b&#39;, c) \in g$. Since we know that $a \Bumpeq_A a$, this means that $b \Bumpeq_B b&#39;$. Then this means that we have $b \Bumpeq_B b&#39;$ and $(b,c) \in g$ and $(b&#39;,c) \in g$, so consequently $b = b&#39;$.)</p>

<p>We now construct equalizers. Suppose we have coherence spaces $A$ and $B$, and morphisms $f, g : A \to B$. Now define the equalizer $(E, e : E \to A)$ as follows. </p>

<ol>
<li><p>For the web, take 
$$E = \left\{ 
\begin{array}{l|c}
&amp; \forall b.\; (a,b) \in f \implies \exists a&#39; \Bumpeq_A a.\; (a&#39;,b) \in g \\
a \in A &amp; \land \\
&amp; \forall b.\; (a,b) \in g \implies \exists a&#39; \Bumpeq_A a.\; (a&#39;,b) \in f \\
\end{array}
\right\}
$$
This picks out the subset of tokens of $A$ on which either $f$ and $g$ agree (up to coherence -- I had this wrong in my first version), or are both undefined. </p></li>
<li><p>Define the coherence relation on $\Bumpeq_E = \{ (a,a&#39;) \in \Bumpeq_A \;|\; a \in E \land a&#39; \in E\}$. This is just the restriction of the coherence relation on $A$ to the subset $E$. This will be reflexive and symmetric since $\Bumpeq_A$ is. </p></li>
<li>The equalizer map $e$ is just the diagonal $e : E \to A = \{(a, a)\;|\;a \in E\}$. </li>
</ol>

<p>Since I messed up my first version of the proof, I'll give the universality property explicitly. Suppose we have any other object $X$ and morphism $m : X \to A$ such that $m;f = m;g$.</p>

<p>Now define $h : X \to E$ as $\{(x,a) \;|\; a \in E\}$. Obviously $h;i \subseteq m$, but to show the equality we need to show the converse $m \subseteq h;i$. </p>

<p>So assume $(x,a) \in m$. We now need to show that $\forall b.\; (a,b) \in f \implies \exists a&#39; \Bumpeq_A a.\; (a&#39;,b) \in g$ and $\forall b.\; (a,b) \in g \implies \exists a&#39; \Bumpeq_A a.\; (a&#39;,b) \in f$. </p>

<p>First, assume $b \in B$ and $(a,b) \in f$. So we know that $(x,a) \in m$ and $(a,b) \in f$, so $(x,b) \in m;f$. Therefore $(x,b) \in m;g$, and so there is an $a&#39; \in A$ such that $(x,a&#39;) \in m$ and $(a&#39;,b) \in g$. Since $x \Bumpeq x$, we know $a \Bumpeq a&#39;$, and so there is an $a&#39; \Bumpeq a$ such that $(a&#39;,b) \in g$. </p>

<p>Symmetrically, assume $b \in B$ and $(a,b) \in g$. So we know that $(x,a) \in m$ and $(a,b) \in g$, so $(x,b) \in m;g$. Therefore $(x,b) \in m;f$, and so there is an $a&#39; \in A$ such that $(x,a&#39;) \in m$ and $(a&#39;,b) \in f$. Since $x \Bumpeq x$, we know $a \Bumpeq a&#39;$, and so there is an $a&#39; \Bumpeq a$ such that $(a&#39;,b) \in f$. </p>

CC BY-SA 2.5
2011-01-21T12:25:34.723Z
I don't see how you can prove $e$ universal. There is only one way to factor any $m : X \rightarrow A$, and that's by setting $h : X \rightarrow E$ as $h := \{(x, a) : (x,a) \in m, a \in E\}$.  Obviously $h;e \subset m$, but I don't see why the converse holds: take some $xma$, and some $b \in B$, with $afb$. Then we have $x(m;f)b$, hence from $m$'s choice we have $x(m;g)b$. From the definition of composition, there exists some $a'$ such that $xma'$ and $a'gb$.  We can deduce that $a \symp a'$, but we only know that $afb$ and $a'gb$, so we can't really deduce that $a=a'$ and finish.
Ohad Kammar
CC BY-SA 2.5
2011-01-21T14:08:02.880Z
Yes, you're right -- the subset the equalizer picks out has to be up to coherence, not equality. I've changed the definition to reflect this, and given the proof the diagram commutes explicitly.
Neel Krishnaswami
CC BY-SA 2.5
2011-01-21T14:15:40.447Z
Ah... But now $e$ doesn't equalise the diagram. Indeed, assume $a(e;f)b$. Then, by $e$'s definition, we have $afb$, hence there exists some $a'\symp a$ such that $a'gb$. But we don't have that $aea'$, so we can't show that $a(e;g)b$. You seem to be running into the same problems I ran into last night, hence my obvious question above.  But perhaps you'll succeed where I failed!  My next step was to take a more sophisticated $e$, say something like $aea' \iff a\symp a'$, but then $e$ is not a valid morphism, so some more careful choice is required.
Ohad Kammar
CC BY-SA 2.5
2011-01-21T17:45:17.673Z
I now remember why I was hoping the answer was in someone's thesis already. :) Anyway, I'll think about it more -- there may be some trick possible via to the fact that inverse images are pairwise incoherent.
Neel Krishnaswami
CC BY-SA 2.5
2011-01-21T11:22:03.900Z
2011-01-21T14:21:45.727Z
2011-01-21T14:21:45.727Z
Neel Krishnaswami
<p>$\newcommand{\symp}{\Bumpeq}$</p>

<p>A coherence relation $\symp_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp_X)$, and a morphism $f : X \to Y$ between coherence spaces is a relation $f \subseteq X \times Y$ such that for all $(x,y) \in f$ and $(x&#39;,y&#39;) \in f$, </p>

<ol>
<li>if $x \symp_X x&#39;$ then $y \symp_Y y&#39;$, and </li>
<li>if $x \symp_X x&#39;$ and $y = y&#39;$ then $x = x&#39;$.</li>
</ol>

<p>The category of coherence spaces is both Cartesian and monoidal closed. I would like to know when pullbacks or pushouts exist for this category, and when some monoidal analogue of pullbacks or pushout exists (and how to define it, in case this notion makes sense).</p>

CC BY-SA 2.5
2011-01-19T14:25:27.173Z
Where is this definition from?  The one in Girard, Lafont & Taylor looks very different.
Charles Stewart
CC BY-SA 2.5
2011-01-19T16:54:08.693Z
The two definitions are equivalent. I'm just taking the web as primitive, from which the set of cliques can be derived.
Neel Krishnaswami
CC BY-SA 2.5
2011-01-19T18:24:24.623Z
I find Neel's choice of definition much more comprehensible than the original.
Dave Clarke
CC BY-SA 2.5
2011-01-19T19:43:38.527Z
@Dave Clarke - I agree.  The first time I read the relevant section in the GLT text, I commented that they should have been called "incoherent spaces" ;-).  Girard's treatment in the Blind Spot (http://iml.univ-mrs.fr/~girard/coursang/coursang.html) is better and more akin to Neel's presentation here.
Marc Hamann
CC BY-SA 2.5
2011-01-21T02:24:13.340Z
I'll state the obvious question: do you know that they don't always exist? In other words, are you familiar with any examples of a functor into coherence relations that doesn't have a limit/colimit?
Ohad Kammar
CC BY-SA 2.5
2011-02-02T12:47:31.220Z
*The two definitions are equivalent* - Right, but did you make up this definition, or did you get it from someone else?  Great question, btw, I'm surprised that no one seems to know whether equalisers always exist.
Charles Stewart
<pl.programming-languages><ct.category-theory><domain-theory><linear-logic>
When do coherence spaces have pullbacks and pushouts?
Neel Krishnaswami
# When do coherence spaces have pullbacks and pushouts?

(Asked by: username_0 on 2011-01-18)

$\newcommand{\symp}{\Bumpeq}$

A coherence relation $\symp\_X$ on a set $X$ is a reflexive and symmetric relation. A coherence space is a pair $(X, \symp\_X)$, and a morphism $f : X \to Y$ between coherence spaces is a relation $f \subseteq X \times Y$ such that for all $(x,y) \in f$ and $(x',y') \in f$,

1. if $x \symp\_X x'$ then $y \symp\_Y y'$, and
2. if $x \symp\_X x'$ and $y = y'$ then $x = x'$.

The category of coherence spaces is both Cartesian and monoidal closed. I would like to know when pullbacks or pushouts exist for this category, and when some monoidal analogue of pullbacks or pushout exists (and how to define it, in case this notion makes sense).

**Tags:** pl.programming-languages, ct.category-theory, domain-theory, linear-logic

> **Comments:**
> **username_1**: Where is this definition from?  The one in Girard, Lafont & Taylor looks very different.  
> **username_0**: The two definitions are equivalent. I'm just taking the web as primitive, from which the set of cliques can be derived.  
> **username_2**: I find Neel's choice of definition much more comprehensible than the original.  
> **username_3**: @username_2 - I agree.  The first time I read the relevant section in the GLT text, I commented that they should have been called "incoherent spaces" ;-).  Girard's treatment in the Blind Spot (http://iml.univ-mrs.fr/~girard/coursang/coursang.html) is better and more akin to Neel's presentation here.  
> **username_4**: I'll state the obvious question: do you know that they don't always exist? In other words, are you familiar with any examples of a functor into coherence relations that doesn't have a limit/colimit?  
> **username_1**: *The two definitions are equivalent* - Right, but did you make up this definition, or did you get it from someone else?  Great question, btw, I'm surprised that no one seems to know whether equalisers always exist.  

---

## 1 answers

### Answer by username_0 on 2011-01-21. Score: 5

I now see how to define equalizers for coherence spaces, which means pullbacks always exist (since products do). I don't know how to do this, actually....

Recall that composition is the usual relational composition, so if $f : A \to B$ and $g : B \to C$, then:

$f ; g = \{(a,c) \in A \times C \;|\; \exists b \in B.\; (a,b) \in f \land (b,c) \in g\}$

(In this definition, the existential actually implies *unique* existence. Suppose that we have $b' \in B$ such that $(a,b') \in f$ and $(b', c) \in g$. Since we know that $a \Bumpeq\_A a$, this means that $b \Bumpeq\_B b'$. Then this means that we have $b \Bumpeq\_B b'$ and $(b,c) \in g$ and $(b',c) \in g$, so consequently $b = b'$.)

We now construct equalizers. Suppose we have coherence spaces $A$ and $B$, and morphisms $f, g : A \to B$. Now define the equalizer $(E, e : E \to A)$ as follows.

1. For the web, take
   $$E = \left\{
   \begin{array}{l|c}
   & \forall b.\; (a,b) \in f \implies \exists a' \Bumpeq\_A a.\; (a',b) \in g \\
   a \in A & \land \\
   & \forall b.\; (a,b) \in g \implies \exists a' \Bumpeq\_A a.\; (a',b) \in f \\
   \end{array}
   \right\}
   $$
   This picks out the subset of tokens of $A$ on which either $f$ and $g$ agree (up to coherence -- I had this wrong in my first version), or are both undefined.
2. Define the coherence relation on $\Bumpeq\_E = \{ (a,a') \in \Bumpeq\_A \;|\; a \in E \land a' \in E\}$. This is just the restriction of the coherence relation on $A$ to the subset $E$. This will be reflexive and symmetric since $\Bumpeq\_A$ is.
3. The equalizer map $e$ is just the diagonal $e : E \to A = \{(a, a)\;|\;a \in E\}$.

Since I messed up my first version of the proof, I'll give the universality property explicitly. Suppose we have any other object $X$ and morphism $m : X \to A$ such that $m;f = m;g$.

Now define $h : X \to E$ as $\{(x,a) \;|\; a \in E\}$. Obviously $h;i \subseteq m$, but to show the equality we need to show the converse $m \subseteq h;i$.

So assume $(x,a) \in m$. We now need to show that $\forall b.\; (a,b) \in f \implies \exists a' \Bumpeq\_A a.\; (a',b) \in g$ and $\forall b.\; (a,b) \in g \implies \exists a' \Bumpeq\_A a.\; (a',b) \in f$.

First, assume $b \in B$ and $(a,b) \in f$. So we know that $(x,a) \in m$ and $(a,b) \in f$, so $(x,b) \in m;f$. Therefore $(x,b) \in m;g$, and so there is an $a' \in A$ such that $(x,a') \in m$ and $(a',b) \in g$. Since $x \Bumpeq x$, we know $a \Bumpeq a'$, and so there is an $a' \Bumpeq a$ such that $(a',b) \in g$.

Symmetrically, assume $b \in B$ and $(a,b) \in g$. So we know that $(x,a) \in m$ and $(a,b) \in g$, so $(x,b) \in m;g$. Therefore $(x,b) \in m;f$, and so there is an $a' \in A$ such that $(x,a') \in m$ and $(a',b) \in f$. Since $x \Bumpeq x$, we know $a \Bumpeq a'$, and so there is an $a' \Bumpeq a$ such that $(a',b) \in f$.

> **Comments:**
> **username_4**: I don't see how you can prove $e$ universal. There is only one way to factor any $m : X \rightarrow A$, and that's by setting $h : X \rightarrow E$ as $h := \{(x, a) : (x,a) \in m, a \in E\}$.  Obviously $h;e \subset m$, but I don't see why the converse holds: take some $xma$, and some $b \in B$, with $afb$. Then we have $x(m;f)b$, hence from $m$'s choice we have $x(m;g)b$. From the definition of composition, there exists some $a'$ such that $xma'$ and $a'gb$.  We can deduce that $a \symp a'$, but we only know that $afb$ and $a'gb$, so we can't really deduce that $a=a'$ and finish.  
> **username_0**: Yes, you're right -- the subset the equalizer picks out has to be up to coherence, not equality. I've changed the definition to reflect this, and given the proof the diagram commutes explicitly.  
> **username_4**: Ah... But now $e$ doesn't equalise the diagram. Indeed, assume $a(e;f)b$. Then, by $e$'s definition, we have $afb$, hence there exists some $a'\symp a$ such that $a'gb$. But we don't have that $aea'$, so we can't show that $a(e;g)b$. You seem to be running into the same problems I ran into last night, hence my obvious question above.  But perhaps you'll succeed where I failed!  My next step was to take a more sophisticated $e$, say something like $aea' \iff a\symp a'$, but then $e$ is not a valid morphism, so some more careful choice is required.  
> **username_0**: I now remember why I was hoping the answer was in someone's thesis already. :) Anyway, I'll think about it more -- there may be some trick possible via to the fact that inverse images are pairwise incoherent.  

---

