Double gluing, coupled with orthogonality, is a method for creating new models of linear logic such as star-polycategories and star-autonomous categories. It is a variation of gluing methods (such as Artin gluing) that works for classical rather than intuitionistic (linear) logic. It is a general method that encompases many existing spaces such as phase spaces, coherence spaces, finiteness spaces, totality spaces, probabilistic coherence spaces?.
Although the name presumably refers to gluing along “two functors at once”, it turns out to also be closely connected to double categories, and in particular to comma double categories.
We begin with the definition of coherence spaces, presented in a way that is amenable to generalization.
If $u\subset X$ and $v\subseteq X$, write $u\perp v$ if $|u\cap v|\leq 1$. Given $U\subseteq P(X)$, let ${U}^\perp=\{v \subseteq X \mid \forall u \in U. u \perp v\}$. Now a coherence space can be given by a set $X$ together with a set $U\subseteq P(X)$ of cliques and a set $V\subseteq P(X)$ of co-cliques that are orthogonal in the sense that $U=V^\perp$ and $V=U^\perp$.
In this presentation of coherence spaces, we can regard $u$ as a relation $1\to X$, and $v$ as a relation $X\to 1$. The relation $\perp$ is then a family of subsets $\perp_X\subseteq [1\to X]\times [X\to 1]$.
Let $C$ be a symmetric monoidal category with an object $I^*$, and let a family $\perp_X\subseteq C(I,X)\times C(X,I^*)$ of relations be given. (For coherence spaces, let $C=Rel$ and $I=I^*$ and $\perp$ be as above.
Let $X$ be an object of $C$. The relation $\perp$ defines a Galois connection between $C(I,X)$ and $C(X,I^*)$ in the usual way: for ${U}\subseteq C(I,X)$ we have ${U}^\perp = \{ v \in C(X,I^*) \mid \forall u\in {U}. u\perp v \}$, and likewise for ${V}\subseteq C(X,J)$ we have ${V}^\perp = \{ u \in C(I,X) \mid \forall v\in {V}. u\perp v \}$.
We define a tight orthogonality space $(X,U,V)$ to be an object $X\in C$ together with ${U}\subseteq C(I,X)$ and ${V}\subseteq C(X,I^*)$ that is a fixed point of this Galois connection, ${U}^\perp = {V}$ and ${V}^\perp= U$.
A morphism between tight orthogonality spaces $(X_1,{U_1},{V_1})\to (X_2,{U_2},{V_2})$ is a morphism $f\in C(X_1,X_2)$ such that
Theorem: (Hyland-Schalk): If an orthogonality $\bot_X\subseteq C(I,X)\times C(X,I^*)$ on a star-autonomous category satisfies four conditions for orthogonalities, a symmetry condition, and a precision condition, then the tight orthogonality spaces form a star-polycategory.
One source of good orthogonality relations $\bot_X\subseteq C(I,X)\times C(X,I^*)$ are the focuses $F\subseteq C(I,I^*)$, from which we can let $u\bot_X v$ if $(v\circ u)\in F$. However, not all the useful orthogonalities arise from focuses.
Let $C$ be any (symmetric) polycategory and $E$ a co-subunary polycategory (i.e. all morphisms have codomain arity 0 or 1), and let $L:C\to Chu(E)$ be a polycategory functor. We consider $C$ as a vertically discrete double polycategory and $L$ as a functor $C\to \mathbb{C}hu(E)$ into the double Chu construction. Similarly, consider $Chu(E)$ as a vertically discrete double polycategory, including into $\mathbb{C}hu(E)$ as the horizontal polycategory.
The double gluing polycategory is then the comma double polycategory (i.e. the comma object in the 2-category of polycategories)
Note that:
If $C$ is a multicategory (i.e. a co-unary polycategory), then so is $Gl(L)$.
If $E$ has a counit that is terminal so that $Chu(E) = Chu(E,1)$, $C$ is a representable multicategory (i.e. a symmetric monoidal category), and $E$ is representable and closed with products so that $Chu(E,1)$ is a $\ast$-autonomous category, then polycategory functors $C\to Chu(E)$ are equivalent to pairs of a lax symmetric monoidal functor $L:C\to E$ and a functor $K:C\to E^{op}$ together with a “contraction” $L(R) \otimes K(R\otimes S) \to K(S)$ satisfying a few axioms. This is how the definition is phrased in Hyland and Schalk.
If $C$ is a $\ast$-polycategory, then $\ast$-polycategory functors $L:C\to Chu(E)$ are equivalent to functors $U_{\le 1} C\to E$ where $U_{\le 1} C$ is the underlying co-subunary polycategory of $C$. If $E$ has a counit that is terminal so that $Chu(E) = Chu(E,1)$, then these are equivalent to multicategory functors $U_{=1} C \to E$. In particular, we can double-glue along any lax symmetric monoidal functor with $\ast$-autonomous domain.
If $C$ and $E$ are closed and representable with sufficient limits and colimits, then one can show (similarly to the conditions for a Chu construction to be representable) that $Gl(L)$ is also representable (as a multicategory or a polycategory, respectively) and closed. Thus, double gluing can produce closed symmetric monoidal and $\ast$-autonomous categories.
The case of double gluing along hom-functors, discussed above, is the case when $E=Set$ so that $Chu(E,1)$ is $\ast$-autonomous, as above, and $L(X) =C(I,X)$ with $K(X) = C(X,I^*)$, together with a restriction that the gluing morphisms be monic (and the additional “orthogonality” restriction.
Last revised on October 14, 2019 at 18:46:06. See the history of this page for a list of all contributions to it.