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 and a functor together with “contractions” (section 4.2.1) — is just a lax symmetric monoidal functor . This explains their observation in section 4.3.1 that when is -autonomous any lax symmetric monoidal extends canonically to a with contraction, by Pavlovic’s observation that 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 as input, which is very unsatisfying. Any ideas?
In particular, the ordinary gluing of would have, as objects, tuples consisting of an object , an object — which is to say two objects — and a morphism in — which is to say morphisms and in . This looks almost like the double gluing except that the morphism goes the wrong way! Unless I am confused somehow.
Ah, I got it! It’s another comma double category. Regarding and as vertically discrete double categories, we can map them both into the double Chu construction (the inclusion of 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 . And to encode the monoidal structure, we can use double polycategories (or multicategories) instead.
1 to 9 of 9