Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

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 comma 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 finite 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 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

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJun 15th 2018
    • (edited Jun 15th 2018)

    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

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeJun 15th 2018

    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.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJun 15th 2018

    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?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJun 16th 2018

    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.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2018

    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.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 16th 2018

    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.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2018

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

    • CommentRowNumber8.
    • CommentAuthorRichard Williamson
    • CommentTimeJun 17th 2018
    • (edited Jun 17th 2018)

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

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJun 22nd 2018

    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”.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJun 22nd 2018
    • (edited Jun 22nd 2018)

    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.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeJun 23rd 2018

    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?

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJun 24th 2018
    • (edited Jun 24th 2018)

    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.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2018

    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 τ n\tau_n is the nn-truncation modality, then a type is τ n\tau_n-separated iff it is an (n+1)(n+1)-type, by definition.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018

    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?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJun 25th 2018

    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 XX is simply connected its pp-localization happens to coincide with the corresponding separated reflection so that there is a dependent elimination principle for the localization.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018
    • (edited Jun 25th 2018)

    they have a “relative” one in which the family lives over the separated reflection instead, and when XX is simply connected its pp-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 nnForum whose mathematical content is not, along the way, being recorded on the nnLab. 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.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJun 25th 2018
    • (edited Jun 25th 2018)

    Thinking about it, did you say that also for pp-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).

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJun 26th 2018

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

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2020

    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 CC is a discrete finite type (h-set) thought of as a type of “colors” and one term g:Cg \colon C of it is thought of as the color “green”, then the CC-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:1Cg: 1 \to C induces g *:H/CHg^{\ast}: \mathbf{H}/C \to \mathbf{H} selecting the gg-fiber. Then composition with its left adjoint, dependent sum, g:HH/C\sum_g: \mathbf{H} \to \mathbf{H}/C, yields the comonadic modal operator, gg *,on\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

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2020

    Looks good to me!

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2020

    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.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeAug 21st 2020

    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 <15\lt 15 pages, with a catchy title.

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 21st 2020

    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.