¿Cuándo tienen espacios de coherencia pullbacks y pushouts?

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

Una relación de coherencia en un conjunto X es una relación reflexiva y simétrica. Un espacio de coherencia es un par (X, \ symp_X) , y un morfismo f: X \ a Y entre espacios de coherencia es una relación f \ subseteq X \ veces Y tal que para todos (x, y) \ en f y (x ', y') \ en f ,$\symp_X$$X$$(X, \symp_X)$$f : X \to Y$$f \subseteq X \times Y$$(x,y) \in f$$(x',y') \in f$

1. si $x \symp_X x'$ entonces $y \symp_Y y'$ , y
2. si $x \symp_X x'$ e $y = y'$ entonces $x = x'$ .

La categoría de espacios de coherencia es tanto cartesiana como monoidal cerrada. Me gustaría saber cuándo existen retrocesos o pushouts para esta categoría, y cuándo existe algún análogo monoidal de retrocesos o pushouts (y cómo definirlo, en caso de que esta noción tenga sentido).

Ahora veo cómo definir ecualizadores para espacios de coherencia, lo que significa que siempre existen retrocesos (ya que los productos sí existen). No sé cómo hacer esto, en realidad ...

Recordemos que la composición es la composición relacional habitual, así que si y , entonces:$f : A \to B$$g : B \to C$

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

(En esta definición, lo existencial en realidad implica existencia única . Supongamos que tenemos tal que y . Ya que sabemos que , esto significa que . Entonces esto significa que tenemos y y , por lo tanto, .)$b' \in B$$(a,b') \in f$$(b', c) \in g$$a \Bumpeq_A a$$b \Bumpeq_B b'$$b \Bumpeq_B b'$$(b,c) \in g$$(b',c) \in g$$b = b'$

Ahora construimos ecualizadores. Supongamos que tenemos espacios de coherencia y , y morfismos . Ahora defina el ecualizador siguiente manera.$A$$B$$f, g : A \to B$$(E, e : E \to A)$

1. Para la web, tome Esto selecciona el subconjunto de tokens de en el que y están de acuerdo (hasta coherencia: me equivoqué en mi primera versión ), o ambos están indefinidos.

   $$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\}$$ $A$$f$$g$

2. Defina la relación de coherencia en . Esto es sólo la restricción de la relación de coherencia en al subconjunto . Esto será reflexivo y simétrico ya que es.$\Bumpeq_E = \{ (a,a') \in \Bumpeq_A \;|\; a \in E \land a' \in E\}$$A$$E$$\Bumpeq_A$

3. El mapa del ecualizador es solo la diagonal .$e$$e : E \to A = \{(a, a)\;|\;a \in E\}$

Como estropeé mi primera versión de la prueba, le daré explícitamente la propiedad de universalidad. Supongamos que tenemos cualquier otro objeto y morfismo tal que .$X$$m : X \to A$$m;f = m;g$

Ahora defina como . Obviamente , pero para mostrar la igualdad necesitamos mostrar el inverso .$h : X \to E$$\{(x,a) \;|\; a \in E\}$$h;i \subseteq m$$m \subseteq h;i$

Entonces supongamos . Ahora necesitamos mostrar que y .$(x,a) \in m$$\forall b.\; (a,b) \in f \implies \exists a' \Bumpeq_A a.\; (a',b) \in g$$\forall b.\; (a,b) \in g \implies \exists a' \Bumpeq_A a.\; (a',b) \in f$

Primero, suponga que y . Así que sabemos que y , por lo que . Por lo tanto , y por lo que hay una tal que y . Como , conocemos , y entonces hay un tal que .$b \in B$$(a,b) \in f$$(x,a) \in m$$(a,b) \in f$$(x,b) \in m;f$$(x,b) \in m;g$$a' \in A$$(x,a') \in m$$(a',b) \in g$$x \Bumpeq x$$a \Bumpeq a'$$a' \Bumpeq a$$(a',b) \in g$

Simétricamente, suponga y . Así que sabemos que y , por lo que . Por lo tanto , y por lo que hay una tal que y . Como , conocemos , y entonces hay un tal que .$b \in B$$(a,b) \in g$$(x,a) \in m$$(a,b) \in g$$(x,b) \in m;g$$(x,b) \in m;f$$a' \in A$$(x,a') \in m$$(a',b) \in f$$x \Bumpeq x$$a \Bumpeq a'$$a' \Bumpeq a$$(a',b) \in f$