Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I finally got around to having a look at the Hyland-Schalk paper. In trying to make abstract sense of it, I realized that (unless I’m mistaken) their input datum for a double gluing construction — a lax symmetric monoidal functor L:C→E and a functor K:C→Eop together with “contractions” L(R)⊗K(R⊗S)→K(S) (section 4.2.1) — is just a lax symmetric monoidal functor C→Chu(E,1). This explains their observation in section 4.3.1 that when C is *-autonomous any lax symmetric monoidal L:C→E extends canonically to a K with contraction, by Pavlovic’s observation that Chu is right adjoint to the forgetful functor from *-autonomous categories to closed symmetric monoidal categories equipped with a chosen object (and morphisms that colaxly preserve the object, which is automatic when the chosen object in the codomain is terminal).
However, so far I haven’t been able to reformulate the actual construction of the double-glued category nicely in terms of this functor C→Chu(E,1) as input, which is very unsatisfying. Any ideas?
In particular, the ordinary gluing of (L,K):C→Chu(E,1) would have, as objects, tuples consisting of an object R∈C, an object (U,X)∈Chu(E,1) — which is to say two objects U,X∈E — and a morphism (U,X)→(L,K)(R) in Chu(E,1) — which is to say morphisms U→L(R) and K(R)→X in E. This looks almost like the double gluing except that the morphism K(R)→X goes the wrong way! Unless I am confused somehow.
Ah, I got it! It’s another comma double category. Regarding C and Chu(E,1) as vertically discrete double categories, we can map them both into the double Chu construction ℂhu(E,1) (the inclusion of Chu(E,1) being an isomorphism onto the horizontal category). Then the double gluing category is the horizontal category of the comma object in double categories (and vertical transformations) of the cospan C→ℂhu(E,1)←Chu(E,1). And to encode the monoidal structure, we can use double polycategories (or multicategories) instead.
1 to 9 of 9