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.
   • CommentAuthorUrs
   • CommentTimeJun 15th 2018
   • (edited Jun 15th 2018)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHow about the terminology "sub-modal object" for a subobject of a modal object? [or maybe better: for which specifically the modality unit is a monomorphism] In line with "subquotient". E.g. concrete objects would be the sub-$\sharp$-modal objects. (or alternatively: _separated modal objects_, in line with separated presheaves ??) <a href="https://ncatlab.org/nlab/revision/diff/modal+type/8">diff</a>, <a href="https://ncatlab.org/nlab/revision/modal+type/8">v8</a>, <a href="https://ncatlab.org/nlab/show/modal+type">current</a>

   How about the terminology “sub-modal object” for a subobject of a modal object?

   [or maybe better: for which specifically the modality unit is a monomorphism]

   In line with “subquotient”.

   E.g. concrete objects would be the sub-$\sharp$-modal objects.

   (or alternatively: separated modal objects, in line with separated presheaves ??)

   diff, v8, current

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeJun 15th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI suppose "sub-modal object" could be okay if the modality is understood. If we want to specify it, then "$\bigcirc$-separated" seems better than "sub-$\bigcirc$-modal". I think we've used "separated" in other places before --- I know Egbert has been studying these in HoTT under that name.

   I suppose “sub-modal object” could be okay if the modality is understood. If we want to specify it, then “$\bigcirc$-separated” seems better than “sub-$\bigcirc$-modal”. I think we’ve used “separated” in other places before — I know Egbert has been studying these in HoTT under that name.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeJun 15th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAlso #1 is a bit confusing; it's a notification from a page edit, but instead of announcing an edit it seems to be asking a question?

   Also #1 is a bit confusing; it’s a notification from a page edit, but instead of announcing an edit it seems to be asking a question?

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJun 16th 2018
   • PermaLink
   Author: Urs
   Format: MarkdownItexSince this entry didn't have a thread yet, I made sure that the right thread is opened by going through the announcement box, not that we get duplicates later.

   Since this entry didn’t have a thread yet, I made sure that the right thread is opened by going through the announcement box, not that we get duplicates later.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJun 16th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't think that's necessary: if there is only one thread with the correct name, then the announcement box should automatically find it.

   I don’t think that’s necessary: if there is only one thread with the correct name, then the announcement box should automatically find it.

6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeJun 16th 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexIt should do what you suggests it does, but it doesn't (all least not always), cf. the [adjoint logic](https://nforum.ncatlab.org/discussion/8596/adjoint-logic/) discussion generated by a change missing the original [adjoint logic](https://nforum.ncatlab.org/discussion/6773/adjoint-logic/) discussion.

   It should do what you suggests it does, but it doesn’t (all least not always), cf. the adjoint logic discussion generated by a change missing the original adjoint logic discussion.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJun 16th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat's because the original discussion wasn't in the "Latest Changes" category.

   That’s because the original discussion wasn’t in the “Latest Changes” category.

8. • CommentRowNumber8.
   • CommentAuthorRichard Williamson
   • CommentTimeJun 17th 2018
   • (edited Jun 17th 2018)
   • PermaLink
   Author: Richard Williamson
   Format: MarkdownItexYes, what Mike writes in #5 and #7 is correct.

   Yes, what Mike writes in #5 and #7 is correct.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJun 22nd 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexBack on #1: in the case of lex modalities, at least, being a sub-type of (i.e. embedding into) a modal type is the same as having modal identity types. The latter condition is extended as a definition of "separated" for arbitrary modalities and even reflective subuniverses e.g. [here](http://luisscoccola.github.io/Luis%20Scoccola_files/localizationHoTT-JMM.pdf). So if you want to talk about subobjects of modal objects for a non-lex modality, where it is a different condition than having modal identity types, then maybe "sub-modal" is in fact better than "separated".

   Back on #1: in the case of lex modalities, at least, being a sub-type of (i.e. embedding into) a modal type is the same as having modal identity types. The latter condition is extended as a definition of “separated” for arbitrary modalities and even reflective subuniverses e.g. here. So if you want to talk about subobjects of modal objects for a non-lex modality, where it is a different condition than having modal identity types, then maybe “sub-modal” is in fact better than “separated”.

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJun 22nd 2018
    • (edited Jun 22nd 2018)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> being a sub-type of (i.e. embedding into) a modal type I am thinking more specifically of the condition that the counit exhibits an embedding.

    being a sub-type of (i.e. embedding into) a modal type

    I am thinking more specifically of the condition that the counit exhibits an embedding.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJun 23rd 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexFor a lex modality, all these conditions are equivalent: embedding into some modal type, the unit being an embedding, and having modal identity types. Do you have an example of a non-lex modality where the unit being an embedding is an important condition?

    For a lex modality, all these conditions are equivalent: embedding into some modal type, the unit being an embedding, and having modal identity types. Do you have an example of a non-lex modality where the unit being an embedding is an important condition?

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJun 24th 2018
    • (edited Jun 24th 2018)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have no good example of submodality in other cases, unfortunately. It just seems that for modal aspects we ought to be taking the behaviour of the unit/counit as primary, since these are what (co)projects out the relevant "modal aspect" of the given object That their behaviour may happen to be equivalent to seemingly weaker-looking conditions seems a convenient accident that one would not want to promote to a definition. Conversely, let me ask you: Do you have a good example of submodal types with non-trivial identity types? You may remember my thoughts on [differential concretification](https://ncatlab.org/nlab/show/concretification#ConcretificationOfDifferentialModuli), which is about finding the right concept of _concrete_, hence of $\sharp$-submodal, for higher homotopy types. The naive idea of the counit being (-1)-truncated, which is what you must have in mind above, does not lead to an interesting condition here.

    I have no good example of submodality in other cases, unfortunately. It just seems that for modal aspects we ought to be taking the behaviour of the unit/counit as primary, since these are what (co)projects out the relevant "modal aspect" of the given object That their behaviour may happen to be equivalent to seemingly weaker-looking conditions seems a convenient accident that one would not want to promote to a definition.

    Conversely, let me ask you: Do you have a good example of submodal types with non-trivial identity types?

    You may remember my thoughts on differential concretification, which is about finding the right concept of concrete, hence of $\sharp$-submodal, for higher homotopy types. The naive idea of the counit being (-1)-truncated, which is what you must have in mind above, does not lead to an interesting condition here.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe condition that I have in mind, which we know has interesting examples outside the lex case, is that of the identity types being modal (commonly called "$\bigcirc$-separated"). One example is the work on localization that I linked to in #9. Another even more basic one is that if $\tau_n$ is the $n$-truncation modality, then a type is $\tau_n$-separated iff it is an $(n+1)$-type, by definition.

    The condition that I have in mind, which we know has interesting examples outside the lex case, is that of the identity types being modal (commonly called “$\bigcirc$-separated”). One example is the work on localization that I linked to in #9. Another even more basic one is that if $\tau_n$ is the $n$-truncation modality, then a type is $\tau_n$-separated iff it is an $(n+1)$-type, by definition.

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018
    • PermaLink
    Author: Urs
    Format: MarkdownItexI did look over the pdf at the link in #9, but I failed to recognize an example beyond that of truncation. (How is the example of submodal truncation interesting, if it just reproduces plain truncation one degree up?) Might there be, besides lightning talk slides, a more comprehensive writeup?

    I did look over the pdf at the link in #9, but I failed to recognize an example beyond that of truncation. (How is the example of submodal truncation interesting, if it just reproduces plain truncation one degree up?) Might there be, besides lightning talk slides, a more comprehensive writeup?

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexNo, not yet, I don't think. The application of the notion in that work is on slide 9: although general reflective subuniverses don't have a dependent elimination principle like monadic modalities, they have a "relative" one in which the family lives over the separated reflection instead, and when $X$ is simply connected its $p$-localization happens to coincide with the corresponding separated reflection so that there is a dependent elimination principle for the localization.

    No, not yet, I don’t think. The application of the notion in that work is on slide 9: although general reflective subuniverses don’t have a dependent elimination principle like monadic modalities, they have a “relative” one in which the family lives over the separated reflection instead, and when $X$ is simply connected its $p$-localization happens to coincide with the corresponding separated reflection so that there is a dependent elimination principle for the localization.

16. • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018
    • (edited Jun 25th 2018)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> they have a "relative" one in which the family lives over the separated reflection instead, and when $X$ is simply connected its $p$-localization happens to coincide with the corresponding separated reflection so that there is a dependent elimination principle for the localization. Thanks for saying this, I would never have extracted that from the slides. Sounds really interesting. There used to be a time when I tried to enforce, only half-jokingly, that there should be no chat on the $n$Forum whose mathematical content is not, along the way, being recorded on the $n$Lab. I have long given up on this, but your recent habit of pointing me to unwritten articles makes me wish we would not completely abandon the idea behind this. It would serve the a constructive communication, I am sure.

    they have a “relative” one in which the family lives over the separated reflection instead, and when $X$ is simply connected its $p$-localization happens to coincide with the corresponding separated reflection so that there is a dependent elimination principle for the localization.

    Thanks for saying this, I would never have extracted that from the slides. Sounds really interesting.

    There used to be a time when I tried to enforce, only half-jokingly, that there should be no chat on the $n$Forum whose mathematical content is not, along the way, being recorded on the $n$Lab. I have long given up on this, but your recent habit of pointing me to unwritten articles makes me wish we would not completely abandon the idea behind this. It would serve the a constructive communication, I am sure.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018
    • (edited Jun 25th 2018)
    • PermaLink
    Author: Urs
    Format: MarkdownItexThinking about it, did you say that also for $p$-localization the sub/separated localization reproduces an ordinary localization? If you allow that degenerate case as "examples" for submodality/separated localization, then I can easily meet your request of examples for submodality/separated localization for non-lex modalities (take any of the modalities on the left boundary of the progression for super-differential cohesion). But isn't this missing the point? An interesting example of submodality/separated localization should be different from an actual localization. Such as concretification on 0-types is. And such as "differential concretification" is on higher homotopy types (at least certain suitably abelian ones).

    Thinking about it, did you say that also for $p$-localization the sub/separated localization reproduces an ordinary localization?

    If you allow that degenerate case as “examples” for submodality/separated localization, then I can easily meet your request of examples for submodality/separated localization for non-lex modalities (take any of the modalities on the left boundary of the progression for super-differential cohesion).

    But isn’t this missing the point? An interesting example of submodality/separated localization should be different from an actual localization. Such as concretification on 0-types is. And such as “differential concretification” is on higher homotopy types (at least certain suitably abelian ones).

18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJun 26th 2018
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat do you mean by "ordinary" or "actual" localization?

    What do you mean by “ordinary” or “actual” localization?

19. • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2020
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI was reading a philosophical paper on properties as 'ways of being', and was reminded of this entry, so thought to add some formal treatment. The paragraph now reads: > For instance if $C$ is a discrete finite [[type]] ([[h-set]]) thought of as a type of "colors" and one [[term]] $g \colon C$ of it is thought of as the color "green", then the $C$-[[dependent type|dependent types]] may be thought of as colored types; and so there is a [[modal operator]] whose modal types are those which are unicolored in green. Hence here the "way of being" expressed by the modality is "being green". (Formally, $g: 1 \to C$ induces $g^{\ast}: \mathbf{H}/C \to \mathbf{H}$ selecting the $g$-fiber. Then composition with its left adjoint, [[dependent sum]], $\sum_g: \mathbf{H} \to \mathbf{H}/C$, yields the comonadic modal operator, $\sum_g \cdot g^{\ast}, on $\mathbf{H}/C$, which acts on a colored type to filter out non-green entities.) Is that right? <a href="https://ncatlab.org/nlab/revision/diff/modal+type/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/modal+type/10">v10</a>, <a href="https://ncatlab.org/nlab/show/modal+type">current</a>

    I was reading a philosophical paper on properties as ’ways of being’, and was reminded of this entry, so thought to add some formal treatment. The paragraph now reads:

    For instance if $C$ is a discrete finite type (h-set) thought of as a type of “colors” and one term $g \colon C$ of it is thought of as the color “green”, then the $C$-dependent types may be thought of as colored types; and so there is a modal operator whose modal types are those which are unicolored in green. Hence here the “way of being” expressed by the modality is “being green”. (Formally, $g: 1 \to C$ induces $g^{\ast}: \mathbf{H}/C \to \mathbf{H}$ selecting the $g$-fiber. Then composition with its left adjoint, dependent sum, $\sum_g: \mathbf{H} \to \mathbf{H}/C$, yields the comonadic modal operator, $\sum_g \cdot g^{\ast}, on$\mathbf{H}/C$, which acts on a colored type to filter out non-green entities.)

    Is that right?

    diff, v10, current

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2020
    • PermaLink
    Author: Urs
    Format: MarkdownItexLooks good to me!

    Looks good to me!

21. • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2020
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThanks for the reassurance. It's very odd reading the philosophical literature on such matters. They're sure that natural language is leading them astray, e.g., here that 'is green' can be construed as a property that an entity 'has'. Then this 'has' seems to be a relation between two 'things', an object and a property. But this leads to worries about how to relate the relation 'has' to the relata, an object and a property. This inclines someone to rewrite the property to 'being green', and so as a kind of way of being, which they hope obviates that issue with relations.

    Thanks for the reassurance. It’s very odd reading the philosophical literature on such matters. They’re sure that natural language is leading them astray, e.g., here that ’is green’ can be construed as a property that an entity ’has’. Then this ’has’ seems to be a relation between two ’things’, an object and a property. But this leads to worries about how to relate the relation ’has’ to the relata, an object and a property. This inclines someone to rewrite the property to ’being green’, and so as a kind of way of being, which they hope obviates that issue with relations.

22. • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2020
    • PermaLink
    Author: Urs
    Format: MarkdownItexYeah, I can imagine a Second Analytical Revolution in Philosophy, with modal type theory reasoning being appreciated. Maybe your book will ignite it? Or maybe one should write a short+clear+crisp note of $\lt 15$ pages, with a catchy title.

    Yeah, I can imagine a Second Analytical Revolution in Philosophy, with modal type theory reasoning being appreciated.

    Maybe your book will ignite it? Or maybe one should write a short+clear+crisp note of $\lt 15$ pages, with a catchy title.

23. • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2020
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI won't hold my breath. There's years and years of accumulated 'wisdom' that would need to be unpicked. Metaphysics, philosophy of language and philosophical logic form an intimately related triad, and (untyped) first-order logic is king. People need to be made to recognise that's something's wrong, that what concerns them in what they're studying can be addressed. I don't see that something brief will do this -- rather a series of interventions to show what is possible when they acknowledge problems, such as the one I did on [category mistakes](https://golem.ph.utexas.edu/category/2020/02/magidor_on_category_mistakes_a.html). Maybe, as with most revolutions, we need the youth to be fired up, but philosophers' formal training is an obstacle.

    I won’t hold my breath. There’s years and years of accumulated ’wisdom’ that would need to be unpicked. Metaphysics, philosophy of language and philosophical logic form an intimately related triad, and (untyped) first-order logic is king. People need to be made to recognise that’s something’s wrong, that what concerns them in what they’re studying can be addressed. I don’t see that something brief will do this – rather a series of interventions to show what is possible when they acknowledge problems, such as the one I did on category mistakes.

    Maybe, as with most revolutions, we need the youth to be fired up, but philosophers’ formal training is an obstacle.