Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeAug 1st 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSzabo's original paper on polycategories contains three interesting things: 1. A claim that every [[distributive category]] yields a polycategory with $C((A_1,\dots,A_n),(B_1,\dots,B_m)) = C(A_1\times\cdots\times A_n, B_1+\cdots+B_m)$. 1. A (mostly incomprehensible) definition of a "Gentzen polycategory" that --- I think --- "has contraction and weakening" in some sense. 1. A claim that every distributive category also yields a Gentzen polycategory. Two questions, then: 1. Since distributive categories are (perhaps surprisingly) *not* actually linearly distributive unless they are posets, it seems likely to me that claim #1 is similarly mistaken. Is that so? 1. Has the definition of "Gentzen polycategory" (or, as I would probably call it, "cartesian polycategory") been taken up anywhere else in the literature? (And maybe, perhaps, written down more readably?)

   Szabo’s original paper on polycategories contains three interesting things:

   1. A claim that every distributive category yields a polycategory with $C((A_1,\dots,A_n),(B_1,\dots,B_m)) = C(A_1\times\cdots\times A_n, B_1+\cdots+B_m)$.
   2. A (mostly incomprehensible) definition of a “Gentzen polycategory” that — I think — “has contraction and weakening” in some sense.
   3. A claim that every distributive category also yields a Gentzen polycategory.

   Two questions, then:

   1. Since distributive categories are (perhaps surprisingly) not actually linearly distributive unless they are posets, it seems likely to me that claim #1 is similarly mistaken. Is that so?
   2. Has the definition of “Gentzen polycategory” (or, as I would probably call it, “cartesian polycategory”) been taken up anywhere else in the literature? (And maybe, perhaps, written down more readably?)
2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 1st 2016
   • (edited Aug 1st 2016)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItex1.) Yes, alas, this seems to be another spot where Szabo did not check his work thoroughly. I guess Cockett and Seely had made the same mistake in the beginning. Really, it's not too surprising. Generally, when you add contraction and weakening into the linear logic mix, the categorical semantics immediately collapses into posetality, like a ruined cake in the oven. (There is Joyal's observation that cartesian $\ast$-autonomous categories are equivalent to Boolean algebras. The proof is easy.) 2.) I'm not aware of anything like that. It doesn't sound very interesting, in view of 1.

   1.) Yes, alas, this seems to be another spot where Szabo did not check his work thoroughly. I guess Cockett and Seely had made the same mistake in the beginning.

   Really, it’s not too surprising. Generally, when you add contraction and weakening into the linear logic mix, the categorical semantics immediately collapses into posetality, like a ruined cake in the oven. (There is Joyal’s observation that cartesian $\ast$-autonomous categories are equivalent to Boolean algebras. The proof is easy.)

   2.) I’m not aware of anything like that. It doesn’t sound very interesting, in view of 1.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeAug 1st 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks! It's not quite completely posetal, I think; isn't there an example in Cockett-Seely of something like categories with biproducts? Even if non-posetal cartesian polycategories aren't so interesting, I would have expected their posetal version to be mentioned more often, since they seem like the natural categorical semantics for classical (non-linear) sequent calculus.

   Thanks! It’s not quite completely posetal, I think; isn’t there an example in Cockett-Seely of something like categories with biproducts?

   Even if non-posetal cartesian polycategories aren’t so interesting, I would have expected their posetal version to be mentioned more often, since they seem like the natural categorical semantics for classical (non-linear) sequent calculus.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeAug 1st 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAlong these lines here is a provocative question: since classical sequent calculus has natural models in distributive lattices, and the natural categorification of a distributive lattice is a distributive category, what is it that makes us believe the usual definition of polycategory is the right categorical structure to serve as semantics for sequent calculus, since it doesn't include distributive categories? Why wouldn't we rather define a polycategory-like structure that *does* include distributive categories?

   Along these lines here is a provocative question: since classical sequent calculus has natural models in distributive lattices, and the natural categorification of a distributive lattice is a distributive category, what is it that makes us believe the usual definition of polycategory is the right categorical structure to serve as semantics for sequent calculus, since it doesn’t include distributive categories? Why wouldn’t we rather define a polycategory-like structure that does include distributive categories?

5. • CommentRowNumber5.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 1st 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexRe #3: sorry -- I was probably partly confused by the distributivity requirement. The other momentary confusion I had has to do with [Blute-Cockett-Seely-Trimble](http://ac.els-cdn.com/002240499500159X/1-s2.0-002240499500159X-main.pdf?_tid=a0f7412e-5835-11e6-b760-00000aacb35f&acdnat=1470089983_7c3e21e9c8753351cb40f912fe6cc5fb), theorem 5.4, which says that the unit of the adjunction between $\ast$-autonomous categories and linearly distributive categories is full and faithful. Apparently I was thinking that when we start with a cartesian linearly distributive category and embed that into the relatively free $\ast$-autonomous category, the latter would still be cartesian. I guess that's not the case then! (Never thought about it before now.)

   Re #3: sorry – I was probably partly confused by the distributivity requirement.

   The other momentary confusion I had has to do with Blute-Cockett-Seely-Trimble, theorem 5.4, which says that the unit of the adjunction between $\ast$-autonomous categories and linearly distributive categories is full and faithful. Apparently I was thinking that when we start with a cartesian linearly distributive category and embed that into the relatively free $\ast$-autonomous category, the latter would still be cartesian. I guess that’s not the case then! (Never thought about it before now.)