# Start a new discussion

## Not signed in

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

## Site Tag Cloud

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

• 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 ??)

• 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 24th 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 $\tau_n$ is the $n$-truncation modality, then a type is $\tau_n$-separated iff it is an $(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 $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.

• 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 $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.

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

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

• CommentRowNumber18.
• CommentAuthorMike Shulman
• CommentTimeJun 25th 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 $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?

• 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 $\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.