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.
   • CommentAuthorUrs
   • CommentTimeFeb 11th 2013
   • (edited Feb 11th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAt _[[2-category equipped with proarrows]]_ in the section _[As a double category](http://ncatlab.org/nlab/show/2-category+equipped+with+proarrows#DefinitionAsDoubleCategory)_ I have made a little change in the labelling: there used to be a horizontal arrow labeled "$K$", but also the ambient 2-category (the one being equipped) is denoted "$K$" and sometimes both symbols, or rather the same symbol with its two different meanings, appeared right next to each other. So I have relabeled the horizontal arrow now to "$J$". I tried to take care to do so consistently throughout the paragraph... Hopefully you can agree with this change. One question: a few months back we chatted vaguely about how equipment data is equivalent to the structure of an internal category in [[Cat]] in the sense at [[internal (infinity,1)-category]]. Back then I had written a quick note on this at _[Segal space - Examples - in 1Grpd](http://ncatlab.org/nlab/show/Segal%20space#ExamplesInIGrpd)_. I'd like to expand on that. Is there meanwhile anything in this direction in the literature?

   At 2-category equipped with proarrows in the section As a double category I have made a little change in the labelling:

   there used to be a horizontal arrow labeled “$K$”, but also the ambient 2-category (the one being equipped) is denoted “$K$” and sometimes both symbols, or rather the same symbol with its two different meanings, appeared right next to each other.

   So I have relabeled the horizontal arrow now to “$J$”. I tried to take care to do so consistently throughout the paragraph… Hopefully you can agree with this change.

   One question: a few months back we chatted vaguely about how equipment data is equivalent to the structure of an internal category in Cat in the sense at internal (infinity,1)-category. Back then I had written a quick note on this at Segal space - Examples - in 1Grpd.

   I’d like to expand on that. Is there meanwhile anything in this direction in the literature?

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeFeb 11th 2013
   • (edited Feb 11th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexSo let's see. A fibrant object in the model structure for category objects internal to the model structure for quasi-categories has as fibrant objects Reedy fibrant objects in $(sSet_{Joyal})^{\Delta^{op}}$ that satisfy the Segal conditions and whose core is a homotopically constant simplicial groupoid. Now in the simple discussion at [Segal space - Examples - in 1Grpd](http://ncatlab.org/nlab/show/Segal%20space#ExamplesInIGrpd) I used that if we restrict this to $(sSet_{Quillen})^{\Delta^{op}}$ then the Reedy fibrancy condition translates right away into the niche-filling condition that characterizes pseudo double categories which correspond to proarrow equipped 2-categories. But in general the niche filling condition says equivalently that $(\partial_0, \partial_1) \colon X_1 \to X_0 \times X_0$ is a Cartesian fibration, right? But the above model structure instead yields a Joyal fibration here, an "inner equifibration". Now of course the two notions don't need to match on the nose. but only up to the relevant notion of equivalent on both sides. But then it's nolonger a straightforward comparison it seems, but may require some work. (?)

   So let’s see. A fibrant object in the model structure for category objects internal to the model structure for quasi-categories has as fibrant objects Reedy fibrant objects in $(sSet_{Joyal})^{\Delta^{op}}$ that satisfy the Segal conditions and whose core is a homotopically constant simplicial groupoid.

   Now in the simple discussion at Segal space - Examples - in 1Grpd I used that if we restrict this to $(sSet_{Quillen})^{\Delta^{op}}$ then the Reedy fibrancy condition translates right away into the niche-filling condition that characterizes pseudo double categories which correspond to proarrow equipped 2-categories.

   But in general the niche filling condition says equivalently that $(\partial_0, \partial_1) \colon X_1 \to X_0 \times X_0$ is a Cartesian fibration, right? But the above model structure instead yields a Joyal fibration here, an “inner equifibration”.

   Now of course the two notions don’t need to match on the nose. but only up to the relevant notion of equivalent on both sides. But then it’s nolonger a straightforward comparison it seems, but may require some work. (?)

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 22nd 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't see any reason for it to match at all if you look at categories in $Cat$ rather than in $Gpd$.

   I don’t see any reason for it to match at all if you look at categories in $Cat$ rather than in $Gpd$.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 22nd 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOh, and thanks for the fix in #1: I think I caught one remaining $K$ that should be a $J$ and fixed it.

   Oh, and thanks for the fix in #1: I think I caught one remaining $K$ that should be a $J$ and fixed it.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 11th 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexFollowing on from the discussion [elsewhere](https://nforum.ncatlab.org/discussion/7026/focusing/?Focus=56860#Comment_56860), it seems not much has been added to the [[proarrow equipment]]/[[framed bicategory]] pages of late. A quick look suggests that polynomial functors and database theory is interested in the idea: [Polynomial functors and polynomial monads](http://arxiv.org/abs/0906.4931), [A Categorical Treatment of Ornaments](http://arxiv.org/abs/1212.3806), [Algebraic Databases](http://arxiv.org/abs/1602.03501). Given the context of that discussion, are there any lessons for type theory from the use of proarrow equipments/framed bicategories? Presumably a framed $(\infty, 2)$-version goes though OK?

   Following on from the discussion elsewhere, it seems not much has been added to the proarrow equipment/framed bicategory pages of late.

   A quick look suggests that polynomial functors and database theory is interested in the idea: Polynomial functors and polynomial monads, A Categorical Treatment of Ornaments, Algebraic Databases.

   Given the context of that discussion, are there any lessons for type theory from the use of proarrow equipments/framed bicategories?

   Presumably a framed $(\infty, 2)$-version goes though OK?

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeApr 11th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe Gambino-Kock paper is neat and would be worth adding a mention of. Algebraic databases is on my reading list, but from what I've heard about it from Patrick it looks very cool too. I think Patrick has a separate preprint on exactness properties for double categories that would be nice to include as well. I haven't encountered the ornaments before. As for lessons for type theory, there are a group of us working on a type theory for equipments as we speak. Further bulletins as events warrant... There should indeed be an ∞-version of this story, but I've never seen it written down. I guess you could start with a Segal object in ∞-Cat as an "∞-double category". Right now I'm more interested in the "homotopy equipment" of ∞-Cat a la Riehl-Verity, which should allow doing ∞-category theory without needing to bother about coherence stuff for the most part.

   The Gambino-Kock paper is neat and would be worth adding a mention of. Algebraic databases is on my reading list, but from what I’ve heard about it from Patrick it looks very cool too. I think Patrick has a separate preprint on exactness properties for double categories that would be nice to include as well. I haven’t encountered the ornaments before.

   As for lessons for type theory, there are a group of us working on a type theory for equipments as we speak. Further bulletins as events warrant…

   There should indeed be an ∞-version of this story, but I’ve never seen it written down. I guess you could start with a Segal object in ∞-Cat as an “∞-double category”. Right now I’m more interested in the “homotopy equipment” of ∞-Cat a la Riehl-Verity, which should allow doing ∞-category theory without needing to bother about coherence stuff for the most part.

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 11th 2016
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI added those references to [[framed bicategory]], but not [[proarrow equipment]].

   I added those references to framed bicategory, but not proarrow equipment.