Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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--modal objects.
(or alternatively: separated modal objects, in line with separated presheaves ??)
I suppose “sub-modal object” could be okay if the modality is understood. If we want to specify it, then “-separated” seems better than “sub--modal”. I think we’ve used “separated” in other places before — I know Egbert has been studying these in HoTT under that name.
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?
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.
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.
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.
That’s because the original discussion wasn’t in the “Latest Changes” category.
Yes, what Mike writes in #5 and #7 is correct.
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”.
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.
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?
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 -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.
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 “-separated”). One example is the work on localization that I linked to in #9. Another even more basic one is that if is the -truncation modality, then a type is -separated iff it is an -type, by definition.
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?
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 is simply connected its -localization happens to coincide with the corresponding separated reflection so that there is a dependent elimination principle for the localization.
they have a “relative” one in which the family lives over the separated reflection instead, and when is simply connected its -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 Forum whose mathematical content is not, along the way, being recorded on the 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.
Thinking about it, did you say that also for -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).
What do you mean by “ordinary” or “actual” localization?
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 is a discrete finite type (h-set) thought of as a type of “colors” and one term of it is thought of as the color “green”, then the -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, induces selecting the -fiber. Then composition with its left adjoint, dependent sum, , yields the comonadic modal operator, \mathbf{H}/C$, which acts on a colored type to filter out non-green entities.)
Is that right?
Looks good to me!
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.
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 pages, with a catchy title.
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.
1 to 23 of 23