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 definitions 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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 object 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
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThis thread is to contiue discussion of [this](https://nforum.ncatlab.org/discussion/7097/polymathlike-project/?Focus=57488#Comment_57488) post of Todd's. My intuition is that internal categories in the effective topos enriched over modest sets ought to work, so I'd like to figure out whether this is true and if not, what goes wrong. According to Hyland's original paper, the internal category of modest sets is locally cartesian closed with finite colimits, and its corresponding indexed category is complete as an indexed category when restricted to the subcategory of separated objects. Moreover, the object of objects is a double-negation sheaf and the object of morphisms is separated, so the whole internal category lives in the category of separated objects as well. Finally, the category of separated objects is, like any category of separated objects for a Lawvere-Tierney topology, a quasitopos. Thus, it seems logical to me to work in the generality of a quasitopos containing an internal category that is cartesian closed with finite colimits and whose corresponding indexed category is complete. Now the most natural way for me to proceed would be to use the machinery of [this paper](http://www.tac.mta.ca/tac/volumes/28/21/28-21abs.html). A cartesian closed internal category gives rise to a symmetric monoidal fibration that is closed in the sense of Theorem 2.14(i), and if it is indexed-complete then it is also closed in the sense of 2.14(ii). By Lemma 2.20, if it is also indexed-cocomplete then its tensor product preserves indexed colimits; indeed it is an "indexed cosmos" in the sense of Def. 2.27. By Lemmas 3.25 and 3.27 there is then a closed bicategory of small enriched categories and profunctors, and by Lemma 11.6 (more or less) it is compact. Finally, by Definition 10.11 and Proposition 10.19, every small enriched category has an "enriched fibration" of presheaves that classifies profunctors by functors. So as I see it, there are the following gaps: * Is an indexed-complete small internal category also indexed-cocomplete? It seems to me that the usual adjoint functor theorem argument should apply. * Is the presheaf fibration "Cauchy complete" in the sense that every left adjoint profunctor into it is representable by a functor? (This step could be skipped if the definition of epistemology were modified to become more equipmenty and talk about functors directly rather than left adjoint profunctors.) I would expect this to be true, since the presheaf fibration is cocomplete (Theorem 10.25). * Is the presheaf fibration equivalent (even Morita equivalent) to a small enriched category? The obvious candidate would be the functor category $M^A$, where $M$ is the internal category of modest sets regarded as self-enriched. For space reasons I left functor categories out of the enriched-indexed paper, but I think they can be defined straightforwardly. So I guess the main question is whether an enriched profunctor can be identified with a functor $B^{op}\times A \to M$. Is there another gap that I've failed to notice?

   This thread is to contiue discussion of this post of Todd’s. My intuition is that internal categories in the effective topos enriched over modest sets ought to work, so I’d like to figure out whether this is true and if not, what goes wrong.

   According to Hyland’s original paper, the internal category of modest sets is locally cartesian closed with finite colimits, and its corresponding indexed category is complete as an indexed category when restricted to the subcategory of separated objects. Moreover, the object of objects is a double-negation sheaf and the object of morphisms is separated, so the whole internal category lives in the category of separated objects as well. Finally, the category of separated objects is, like any category of separated objects for a Lawvere-Tierney topology, a quasitopos. Thus, it seems logical to me to work in the generality of a quasitopos containing an internal category that is cartesian closed with finite colimits and whose corresponding indexed category is complete.

   Now the most natural way for me to proceed would be to use the machinery of this paper. A cartesian closed internal category gives rise to a symmetric monoidal fibration that is closed in the sense of Theorem 2.14(i), and if it is indexed-complete then it is also closed in the sense of 2.14(ii). By Lemma 2.20, if it is also indexed-cocomplete then its tensor product preserves indexed colimits; indeed it is an “indexed cosmos” in the sense of Def. 2.27. By Lemmas 3.25 and 3.27 there is then a closed bicategory of small enriched categories and profunctors, and by Lemma 11.6 (more or less) it is compact. Finally, by Definition 10.11 and Proposition 10.19, every small enriched category has an “enriched fibration” of presheaves that classifies profunctors by functors.

   So as I see it, there are the following gaps:

   • Is an indexed-complete small internal category also indexed-cocomplete? It seems to me that the usual adjoint functor theorem argument should apply.
   • Is the presheaf fibration “Cauchy complete” in the sense that every left adjoint profunctor into it is representable by a functor? (This step could be skipped if the definition of epistemology were modified to become more equipmenty and talk about functors directly rather than left adjoint profunctors.) I would expect this to be true, since the presheaf fibration is cocomplete (Theorem 10.25).
   • Is the presheaf fibration equivalent (even Morita equivalent) to a small enriched category? The obvious candidate would be the functor category $M^A$, where $M$ is the internal category of modest sets regarded as self-enriched. For space reasons I left functor categories out of the enriched-indexed paper, but I think they can be defined straightforwardly. So I guess the main question is whether an enriched profunctor can be identified with a functor $B^{op}\times A \to M$.

   Is there another gap that I’ve failed to notice?

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexMike, before I attempt to engage with your fine response, I just wanted to **thank you** for taking the time. I'm actually a bit touched that you and Richard would take an interest in this! It would come as a *big* relief to me if this problem were solved. I might be a little slow in responding adequately however.

   Mike, before I attempt to engage with your fine response, I just wanted to thank you for taking the time. I’m actually a bit touched that you and Richard would take an interest in this!

   It would come as a big relief to me if this problem were solved.

   I might be a little slow in responding adequately however.

3. • CommentRowNumber3.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexLooking now at the second bullet point, I agree that it would be worthwhile to write out an equipment version of epistemology. For that matter, someone should add the relevant material to [[cartesian bicategory]], since that notion is actually tested and documented. (I've not looked at the Carboni-Kelly-Verity-Wood paper to see what they do.)

   Looking now at the second bullet point, I agree that it would be worthwhile to write out an equipment version of epistemology. For that matter, someone should add the relevant material to cartesian bicategory, since that notion is actually tested and documented. (I’ve not looked at the Carboni-Kelly-Verity-Wood paper to see what they do.)

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexIt might be helpful to start a page [[epistemology]].

   It might be helpful to start a page epistemology.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWell, this idea is closely related to a number of other things that have been on my mind, including equipments, formal category theory, enriched indexed categories, and foundational/size questions, so it has some intrinsic interest for me. I recall reading about epistemologies on your personal web a little while ago but not really engaging with the idea, possibly because at the time I was still too antagonistic towards the V-Mod approach to formal category theory (I went through a stage of great annoyance that so many people were content to just disregard functors in favor of profunctors with an unsatisfying wave at "well, Cauchy-completeness is a very mild condition" -- now I am perhaps a little more forgiving (-: ). Anyway, you could start a page about them by copying some of the material from your personal web.

   Well, this idea is closely related to a number of other things that have been on my mind, including equipments, formal category theory, enriched indexed categories, and foundational/size questions, so it has some intrinsic interest for me. I recall reading about epistemologies on your personal web a little while ago but not really engaging with the idea, possibly because at the time I was still too antagonistic towards the V-Mod approach to formal category theory (I went through a stage of great annoyance that so many people were content to just disregard functors in favor of profunctors with an unsatisfying wave at “well, Cauchy-completeness is a very mild condition” – now I am perhaps a little more forgiving (-: ). Anyway, you could start a page about them by copying some of the material from your personal web.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI remember some of that frustration, although it was probably toned down at the nForum. Anyway, I agree with you now that one might as well do it right and gain the extra generality, even if it costs a few more keystrokes. I made a small start at [[epistemology]], using the language of proarrow equipment as opposed to framed bicategories since the notion of potency seems very straightforward in that language. But it might be advantageous rephrasing in terms of framed bicategories in view of where you and Richard might want to take it (3-categorical considerations).

   I remember some of that frustration, although it was probably toned down at the nForum. Anyway, I agree with you now that one might as well do it right and gain the extra generality, even if it costs a few more keystrokes.

   I made a small start at epistemology, using the language of proarrow equipment as opposed to framed bicategories since the notion of potency seems very straightforward in that language. But it might be advantageous rephrasing in terms of framed bicategories in view of where you and Richard might want to take it (3-categorical considerations).

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeMay 9th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThanks! Do you really mean in the "Idea" section to say that it is a cartesian bicategory? Your definition doesn't seem to necessarily be cartesian. The extra condition that the adjunction be lax-idempotent is a bit mysterious to me. But it reminds me of something else. When I was working out the general theory of "presheaf objects" in a (virtual) equipment, I found that it wasn't enough for the presheaf object to just be a representing object for the pseudofunctor of modules (Prop. 10.19 of the enriched indexed paper); the fully-faithfulness of that representation had to also be internalized in terms of the closed structure of the bicategory of modules (Prop. 10.18). (From a type-theoretic perspective, this extra condition is a form of univalence / function extensionality.) I don't suppose there is any chance that these two extra conditions are equivalent? Or, maybe more plausibly, that the extra conditions on each side are exactly what's needed to make the two definitions coincide?

   Thanks! Do you really mean in the “Idea” section to say that it is a cartesian bicategory? Your definition doesn’t seem to necessarily be cartesian.

   The extra condition that the adjunction be lax-idempotent is a bit mysterious to me. But it reminds me of something else. When I was working out the general theory of “presheaf objects” in a (virtual) equipment, I found that it wasn’t enough for the presheaf object to just be a representing object for the pseudofunctor of modules (Prop. 10.19 of the enriched indexed paper); the fully-faithfulness of that representation had to also be internalized in terms of the closed structure of the bicategory of modules (Prop. 10.18). (From a type-theoretic perspective, this extra condition is a form of univalence / function extensionality.) I don’t suppose there is any chance that these two extra conditions are equivalent? Or, maybe more plausibly, that the extra conditions on each side are exactly what’s needed to make the two definitions coincide?

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeMay 10th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexThe definition at my nLab web page does not include the cartesian bicategory condition. But as I just finished explaining in response to Richard over at the other thread, I think the cartesian bicategory case is what makes the problem of existence much more interesting (and hard). I'll have to dig into your papers to see exactly what you're referring to here, but as you know free cocompletion monads are KZ/lax-idempotent in general, and free cocompletion is what I'm making the axiomatic starting point of this synthetic enriched category theory. Does that help remove some of the mystery? Let me think some more on what you're wondering about here; it sounds interesting! But a propos of this, let me pop a question back to you. We are wondering in #1 about cocompleteness of the base of enrichment (which is $p 1$ in our set-up). But really I sense that it's *total cocompleteness* that is at stake, since the algebras of the KZ monad are totally complete (algebra structure being left adjoint to the unit which is the formal yoneda embedding $y a: a \to p a$). So my question is along the lines of: does it make sense to speak of internal categories being totally cocomplete? I'm not sure how to say it fibrationally. That's what I was getting at when I vaguely said that I got the sense that (co)completeness of the internal category of modest sets, whatever it means in Hyland's papers, might not mean something strong enough for our purposes. I think we want totality and cototality, whatever that might for internal categories.

   The definition at my nLab web page does not include the cartesian bicategory condition. But as I just finished explaining in response to Richard over at the other thread, I think the cartesian bicategory case is what makes the problem of existence much more interesting (and hard).

   I’ll have to dig into your papers to see exactly what you’re referring to here, but as you know free cocompletion monads are KZ/lax-idempotent in general, and free cocompletion is what I’m making the axiomatic starting point of this synthetic enriched category theory. Does that help remove some of the mystery?

   Let me think some more on what you’re wondering about here; it sounds interesting!

   But a propos of this, let me pop a question back to you. We are wondering in #1 about cocompleteness of the base of enrichment (which is $p 1$ in our set-up). But really I sense that it’s total cocompleteness that is at stake, since the algebras of the KZ monad are totally complete (algebra structure being left adjoint to the unit which is the formal yoneda embedding $y a: a \to p a$). So my question is along the lines of: does it make sense to speak of internal categories being totally cocomplete? I’m not sure how to say it fibrationally.

   That’s what I was getting at when I vaguely said that I got the sense that (co)completeness of the internal category of modest sets, whatever it means in Hyland’s papers, might not mean something strong enough for our purposes. I think we want totality and cototality, whatever that might for internal categories.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeMay 10th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe argument that a symmetric monoidal category is compact iff its delooping is potent is cute. (I get less confused if I distinguish between a monoidal category and its delooping into a one-object bicategory.) I can see that you want some stronger assumption to avoid this case. But since there are (of course) interesting examples of enrichments that aren't cartesian, it would be nice if there were some condition weaker than cartesianness that suffices to make the notion strong.

   The argument that a symmetric monoidal category is compact iff its delooping is potent is cute. (I get less confused if I distinguish between a monoidal category and its delooping into a one-object bicategory.) I can see that you want some stronger assumption to avoid this case. But since there are (of course) interesting examples of enrichments that aren’t cartesian, it would be nice if there were some condition weaker than cartesianness that suffices to make the notion strong.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe puzzling thing to me about lax-idempotence is not that the monad is lax-idempotent, but that we have to assume that explicitly rather than getting it for free, since the right adjoint is defined as a "classifier for profunctors" and cocompleteness is defined in terms of profunctors. But thinking about it some more, I think this condition is indeed closely related to the one I mentioned. The universal property of my Prop 10.19 should say, in your language, exactly that $i$ has a right adjoint. Then Prop 10.18 follows from its own special case when $f=g=1_{p a}$, which says equivalently that $1_{p a}$ is a right lifting of $e a$ along itself. The special case when $f=1_{p a}$ and $g=y a$ says that $i(y a)$ is a right lifting of $1_a$ along $e a$, i.e. that $i(y a)$ is left adjoint to $e a$, which I think you said is equivalent to lax-idempotence. The more general case $f=g=1_{p a}$ can be interpreted to say that $y a$ is *dense*. Does this follow from lax-idempotence alone?

    The puzzling thing to me about lax-idempotence is not that the monad is lax-idempotent, but that we have to assume that explicitly rather than getting it for free, since the right adjoint is defined as a “classifier for profunctors” and cocompleteness is defined in terms of profunctors. But thinking about it some more, I think this condition is indeed closely related to the one I mentioned. The universal property of my Prop 10.19 should say, in your language, exactly that $i$ has a right adjoint. Then Prop 10.18 follows from its own special case when $f=g=1_{p a}$, which says equivalently that $1_{p a}$ is a right lifting of $e a$ along itself. The special case when $f=1_{p a}$ and $g=y a$ says that $i(y a)$ is a right lifting of $1_a$ along $e a$, i.e. that $i(y a)$ is left adjoint to $e a$, which I think you said is equivalent to lax-idempotence. The more general case $f=g=1_{p a}$ can be interpreted to say that $y a$ is dense. Does this follow from lax-idempotence alone?

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 10th 2016
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRegarding totality, I agree that the cocompleteness of presheaf objects in an epistemelogy is "total" in a certain sense, but it seems to me that that totality is *relative to the epistemology* (the current "base of enrichment"). In the case of modest sets, we would be asking for totality of modest sets relative to modest sets, not relative to the whole effective topos. And in classical enriched category theory, *any* cosmos $V$ is total *qua* $V$-enriched category, whether or not it is total *qua* Set-enriched category.

    Regarding totality, I agree that the cocompleteness of presheaf objects in an epistemelogy is “total” in a certain sense, but it seems to me that that totality is relative to the epistemology (the current “base of enrichment”). In the case of modest sets, we would be asking for totality of modest sets relative to modest sets, not relative to the whole effective topos. And in classical enriched category theory, any cosmos $V$ is total qua $V$-enriched category, whether or not it is total qua Set-enriched category.

12. • CommentRowNumber12.
    • CommentAuthorRichard Williamson
    • CommentTimeMay 14th 2016
    • (edited May 14th 2016)
    • PermaLink
    Author: Richard Williamson
    Format: MarkdownItexMy apologies for the delayed reply, it was a hectic week. Thanks very much for your reply to my question in the other thread Todd, it was very helpful! I realised after posting the question that a one-object cartesian bicategory might not be the same as a cartesian monoidal category (I was a bit quick when looking things up!); many thanks for taking this as a point of departure to say a lot of interesting and useful things! I remain very much interested in this, and wil try to make a more substantial contribution soon.

    My apologies for the delayed reply, it was a hectic week.

    Thanks very much for your reply to my question in the other thread Todd, it was very helpful! I realised after posting the question that a one-object cartesian bicategory might not be the same as a cartesian monoidal category (I was a bit quick when looking things up!); many thanks for taking this as a point of departure to say a lot of interesting and useful things!

    I remain very much interested in this, and wil try to make a more substantial contribution soon.