You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Morgan Rogers (he/him) (Apr 11 2020 at 09:14):Ha well it sounds like you've answered most of the questions I mentioned, good job! @Axel Osmond mentioned to me a while ago that Anel and a collaborator had something relating to the plus construction in the works. A comment, then:
I just traced back the name "modality" you mention to Section 7.7 of the HoTT book; there they introduce operations on the universe of types that behave (syntactically) like the familiar operators from modal logic, and there is a passing comment that they induce pullback-stable orthogonal factorisation systems. In A Generalized Blakers-Massey Theorem by Anel, Biedermann, Finster and Joyal, they name such factorisation systems "modalities"; in my opinion this is a rather lazy and misleading choice of terminology (which your paper has unfortunately inherited) since there is no longer anything resembling a modal operator involved, and there are plenty of properly-motivated naming conventions for orthogonal factorisation systems out there. What's doubly confusing is that your paper examines generalized plus constructions, which being unary operators could be compared to modalities in the original sense :face_palm:
Is there any other motivation for the choices of names in your paper?
Chaitanya Leena Subramaniam (Apr 11 2020 at 09:29):Morgan Rogers said:
Ha well it sounds like you've answered most of the questions I mentioned, good job! Axel Osmond mentioned to me a while ago that Anel and a collaborator had something relating to the plus construction in the works. A comment, then:
I just traced back the name "modality" you mention to Section 7.7 of the HoTT book; there they introduce operations on the universe of types that behave (syntactically) like the familiar operators from modal logic, and there is a passing comment that they induce pullback-stable orthogonal factorisation systems. In A Generalized Blakers-Massey Theorem by Anel, Biedermann, Finster and Joyal, they name such factorisation systems "modalities"; in my opinion this is a rather lazy and misleading choice of terminology (which your paper has unfortunately inherited) since there is no longer anything resembling a modal operator involved, and there are plenty of properly-motivated naming conventions for orthogonal factorisation systems out there. What's doubly confusing is that your paper examines generalized plus constructions, which being unary operators could be compared to modalities in the original sense :face_palm:
Is there any other motivation for the choices of names in your paper?
The two notions of modality are exactly the same when the underlying -category is an -topos (which is all that HoTT can talk about, hence it doesn't make sense to compare them otherwise). So the choice of terminology is perfectly consistent :P
In the case of an -topos, the internal modal operator is the reflection seen as an endomorphism of the universe of the -topos (which is representable --- at least a universe classifying sufficiently small objects). The modalities of ABFJ have the advantage of making sense in other -categories than -topoi. Of course, in these categories the universe is no longer representable (no descent) so there is no internal modal operator, but the external one still exists --- it is the idempotent monad corresponding to the reflection.
Morgan Rogers (he/him) (Apr 11 2020 at 09:40):Sorry, but I don't think "they coincide in the situation I care about, so it's fine" is a good excuse for giving two clearly different things the same name. Conflation is already a big problem in mathematics even though we have complete freedom to choose how we name things! Weren't these some of the same people that decided we should introduce the name "logos" for the objects in the opposite of the category of toposes?
Morgan Rogers (he/him) (Apr 11 2020 at 09:43):Orthogonal factorisation systems stable under pullback make sense in much simpler categories; Thollen presented some work on very general factorisation systems at the last PSSL, for example.
Morgan Rogers (he/him) (Apr 11 2020 at 09:45):In any case, naming aside, I look forward to giving this paper a good read.
Chaitanya Leena Subramaniam (Apr 11 2020 at 10:27):I agree that conflation can sometimes be an issue, but I somewhat disagree that it is one in this particular case (or it's at most a minor issue). On the one hand, the equivalence between modalities qua modal operators and pullback-stable factorisation systems is already part of HoTT-literature : cf. section 1 of https://arxiv.org/abs/1706.07526 (I guess you already know this paper)
Secondly, it's more like "they coincide in every situation where both make sense".
Morgan Rogers (he/him) (Apr 11 2020 at 10:56):The fact that every X corresponds to a Y still doesn't seem like good justification for giving X and Y the same name, since it amounts to claiming that this equivalence is somehow obvious or trivial, and takes the work required to prove that result for granted. The figure on page 2:9 of the paper you just shared shows that the authors take 4 theorems at least to prove a cycle of equivalences, and moreover that they do not commit the same problematic conflation that I'm complaining about.
Also, the idea that unary/modal operators and factorisation systems only both make sense in the context of infinity topoi seems pretty farfetched.
I'm aware that I'm sending a lot of negative energy out with this argument; it turns out the naming of things is something I'm more passionate about than I had realised.
Chaitanya Leena Subramaniam (Apr 11 2020 at 12:50):I'm aware that I'm sending a lot of negative energy out with this argument; it turns out the naming of things is something I'm more passionate about than I had realised.
No problem :wink: names of things are very important