Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthormaxsnew
   • CommentTimeDec 12th 2017
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexMade a stub for [[admissible rule]] with a few examples, after seeing the discussion about negation [here](https://nforum.ncatlab.org/discussion/8156/string-diagrams-for-linearly-distributive-categories-with-unit-counit/#Item_15)

   Made a stub for admissible rule with a few examples, after seeing the discussion about negation here

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeDec 12th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks! I tweaked it a little. I wasn't sure what you meant by "strictness" so I replaced it by a sentence that I do understand; can you explain what you meant?

   Thanks! I tweaked it a little. I wasn’t sure what you meant by “strictness” so I replaced it by a sentence that I do understand; can you explain what you meant?

3. • CommentRowNumber3.
   • CommentAuthormaxsnew
   • CommentTimeDec 13th 2017
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexI was basically trying to say what you did in the edit. Initially I wrote that admissible or not should not affect what is considered a model (for the "specified" admissible rules), but thinking about cut in particular, a 1-variable sequent calculus with admissible cut can only have models where composition is strictly associative, but if cut is a primitive rule then you can make a distinction between (cut;cut);cut and cut;(cut;cut), so you could have models that are weakly associative. I'm not sure if that's a sensible distinction though because if you *do* want composition to be associative you should add equalities for it.

   I was basically trying to say what you did in the edit. Initially I wrote that admissible or not should not affect what is considered a model (for the “specified” admissible rules), but thinking about cut in particular, a 1-variable sequent calculus with admissible cut can only have models where composition is strictly associative, but if cut is a primitive rule then you can make a distinction between (cut;cut);cut and cut;(cut;cut), so you could have models that are weakly associative. I’m not sure if that’s a sensible distinction though because if you do want composition to be associative you should add equalities for it.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeDec 14th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't agree that an admissible cut can only have models where composition is strictly associative. In fact, I think it's *easier* to deal with non-strict models when cut is admissible than when it's not, since in the former case you don't have to put the associativity isomorphisms and their coherence into the syntax. As a simple example, the free category on a graph is also the free bicategory on the same graph (in the appropriate weak bicategorical sense), and you can prove that by induction over a cut-free presentation of it, which essentially amounts to choosing to bracket all composites in one direction.

   I don’t agree that an admissible cut can only have models where composition is strictly associative. In fact, I think it’s easier to deal with non-strict models when cut is admissible than when it’s not, since in the former case you don’t have to put the associativity isomorphisms and their coherence into the syntax. As a simple example, the free category on a graph is also the free bicategory on the same graph (in the appropriate weak bicategorical sense), and you can prove that by induction over a cut-free presentation of it, which essentially amounts to choosing to bracket all composites in one direction.

5. • CommentRowNumber5.
   • CommentAuthormaxsnew
   • CommentTimeDec 15th 2017
   • PermaLink
   Author: maxsnew
   Format: MarkdownItexHm, I guess you're right, as long as you relax the strictness of you notion of model it doesn't matter if the syntax is strict? Would another example be that the free strictly associative monoidal category is also the free monoidal category, but crucially the former has functors that strictly preserve the monoid whereas the latter only pseudo preserves them?

   Hm, I guess you’re right, as long as you relax the strictness of you notion of model it doesn’t matter if the syntax is strict? Would another example be that the free strictly associative monoidal category is also the free monoidal category, but crucially the former has functors that strictly preserve the monoid whereas the latter only pseudo preserves them?

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeDec 16th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYes, that's right.

   Yes, that’s right.