Kiedy przestrzenie spójności mają wycofania i wypychania?

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

Relacja koherencji $\symp_X$ na zbiorze $X$ jest relacją zwrotną i symetryczną. Przestrzeń koherencji to para $(X, \symp_X)$ , a morfizm $f : X \to Y$ między przestrzeniami koherencji jest relacją $f \subseteq X \times Y$ taką, że dla wszystkich $(x,y) \in f$ i $(x',y') \in f$ ,

1. jeśli $x \symp_X x'$ to $y \symp_Y y'$ , i
2. jeśli $x \symp_X x'$ i $y = y'$ to $x = x'$ .

Kategoria przestrzeni koherencji jest zarówno kartezjańska, jak i monoidalna zamknięta. Chciałbym wiedzieć, kiedy dla tej kategorii istnieją wycofania lub wypychania i kiedy istnieje jakiś monoidalny analog wycofań lub wypychań (i jak to zdefiniować, na wypadek, gdyby to pojęcie miało sens).

Widzę teraz, jak zdefiniować korektory dla przestrzeni koherencji, co oznacza, że ​​zawsze istnieją niedociągnięcia (ponieważ produkty mają). Właściwie to nie wiem jak to zrobić ...

Przypomnijmy, że kompozycja ma zwykle skład relacyjny więc jeśli i , a następnie:$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\}$

(W tej definicji egzystencjalność w rzeczywistości implikuje wyjątkowe istnienie. Załóżmy, że mamy tak że i . Ponieważ wiemy, że , oznacza to, że . To oznacza, że ​​mamy i oraz , a zatem konsekwentnie .)$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'$

Teraz konstruujemy korektory. Załóżmy, że mamy przestrzenie spójność i oraz morfizmów . Teraz zdefiniuj korektor w następujący sposób.$A$$B$$f, g : A \to B$$(E, e : E \to A)$

1. W przypadku sieci weź Wyodrębnia to podzbiór tokenów na który zgadzają się albo i (do spójności - pomyliłem się w mojej pierwszej wersji ) lub oba są niezdefiniowane.

   $$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. Zdefiniuj relację koherencji na . To jest po prostu ograniczenie relacji koherencji na do podzbioru . Będzie to zwrotne i symetryczne, ponieważ jest.$\Bumpeq_E = \{ (a,a') \in \Bumpeq_A \;|\; a \in E \land a' \in E\}$$A$$E$$\Bumpeq_A$

3. Mapa korektora to tylko przekątna .$e$$e : E \to A = \{(a, a)\;|\;a \in E\}$

Ponieważ pomieszałem moją pierwszą wersję dowodu, podam jawnie właściwość uniwersalności. Załóżmy, że mamy jakikolwiek inny obiekt i morfizm taki, że .$X$$m : X \to A$$m;f = m;g$

Teraz zdefiniuj jako . Oczywiście , ale aby pokazać równość, musimy pokazać odwrotność .$h : X \to E$$\{(x,a) \;|\; a \in E\}$$h;i \subseteq m$$m \subseteq h;i$

Załóżmy więc . Musimy teraz pokazać, że oraz .$(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$

Najpierw załóżmy i . Wiemy, że i , SO . Dlatego , a więc nie jest tak że i . Ponieważ , wiemy'a więc nie jest takie, że .$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$

Symetrycznie załóżmy i . Wiemy więc, że oraz , więc . Dlatego , a więc istnieje takie jak oraz . Ponieważ , wiemy , a więc istnieje taki, że .$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$