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.
1 to 33 of 33
The referee of BFP in RCoHoTT complained (quite justifiably) that sometimes I call a modality and sometimes a comodality, and that the terminology should be consistent. But I am torn as to which to use, i.e. whether the word “modality” should include comonadic ones as well as monadic ones. On one hand, talking about “modalities” and “comodalities” is usually more concise and euphonious than “monadic modalities” and “comonadic modalities”. But on the other hand, in traditional modal logic, both monads like and comonads like are called “modalities”, and it’s not very concise or euphonious either to have to say “modalities and comodalities” when talking about a collection like that includes some of each sort.
Would it be a terrible thing to coin words like “monadality” and “comonadality” for the case when we want to indicate the handedness?
Not terrible, no.
“Monadality” would suggest that there is a word “monadal”. I wouldn’t want monadicity” though.
We speak of “lions” in general when we may have distinguished lions and lionesses in a text. But I guess we need more precision here.
You’d think at first glance that this problem would arise frequently in category theory, but maybe referring to X and co-X together is not so common.
Category theory has the advantage that an X in is generally the same as a co-X in , so that X’s in general include co-X’s by changing the underlying category. Unfortunately that isn’t really the case in the internal language any more.
Would “monadality” mean something different than “idempotent monad”?
In cases like this I like to write “(co-)struc”. As in
Consider the Eilenberg-Moore category of a (co-)monad. Then the (co-)free (co-)algebras are those in the image of the embedding of the (co-)Kleisli category.
Would “monadality” mean something different than “idempotent monad”?
Yes, I think a monadality would be the things that the HoTT Book calls “modalities”, which are not just idempotent monads even internally (those are the “reflective subuniverses”).
Generally, when it comes to decrying hybrids like “television”, “heterosexual”, and “sociology”, I feel that ship has already sailed – the issue should be more of triggering the right sorts of associations.
Re: #1, As you say, both and are called “modalities” in ordinary modal logic, which would seem to suggest calling both and “modalities”. If you like the term “comodality”, perhaps you could introduce it explicitly as an abbreviation for “comonadic modality”?
That would have the unfortunate consequence that a “comodality” is a special kind of “modality”, which goes against (almost?) all categorical precedent for the prefix “co-“.
I would tend to view that more as a reason not to like the neologism “comodality”, rather than a reason not to use the term “modality” for . There doesn’t seem to be any reason to prefer the term “modality” for over other than the fact that “monad” and “modal” sound similar.
Yes, I’m also leaning in that direction. Monadic modalities do have the advantage of being easy to describe in the internal type theory, whereas nontrivial comonadic ones can’t really be done cleanly without modifying the judgmental structure. I think when we wrote the HoTT Book, we used “modality” for the monadic ones because we didn’t really know a good way to describe the comonadic ones at all. So probably I will use “modality” for both when in a context like spatial or real-cohesive type theory where both exist, but continue to use “modality” for the monadic ones (with a terminological note at the beginning) when those are the only ones being studied.
Well, the specific confusing situation from #1 that the referee complained about, where was sometimes called a modality and sometimes a comodality, will no longer obtain. The word “comodality” won’t be used; will be a modality, or a comonadic modality if needed to distinguish. The only potential confusion is that in some contexts “modality” may mean what in other contexts would have to be distinguished as a “monadic modality”. But as long as each paper is internally consistent and declares its terminology at the beginning, I don’t think that will be worse than other “local abuses of terminology” that are common in mathematics, such as how “space” might mean “topological space”, “pointed compactly generated space”, or “simplicial set” depending on context.
Late to this discussion. Just to say that I see only one way to complete the pattern.
| unit | counit |
| reflection | coreflection |
| localization | colocalization |
| modality | ?!? |
| reflective subcategory | coreflective subcategory (not cosubcategory) |
| monadic functor | comonadic functor (not monadic cofunctor) |
And the point, if I need to say it again, is that it’s wrong to even start out by putting “modality” in the left-hand column. The word “modality” should label the entire row.
not cosubcategory
The reason that one does not say “cosubcategory” here is because the concept of full subcategory does not change under passing to opposite categories. But the concepts in the list become “co” under passing to the opposite category.
it’s wrong
Could you remind me by which rules this is wrong?
The reason that one does not say “cosubcategory” here is because the concept of full subcategory does not change under passing to opposite categories. But the concepts in the list become “co” under passing to the opposite category.
Exactly. The point is that the concept of “modality” does not change either. The concept of “monadic modality” does change; it changes to a “comonadic modality”. The reason it’s wrong to say “modality” to mean only the monadic sort is that for the entire history of modal logic the word “modality” has referred both to the monadic sort (e.g. ) and to the comonadic sort (e.g. ).
The reason it’s wrong to say “modality” to mean only the monadic sort is … history
I suggest to exercise restraint in calling people wrong on the basis that their suggestions don’t comply with, of all things, history.
The use of “colimit” for some types of limits wasn’t and isn’t universally practiced either, and so what.
I am happy to accept your tastes, especially if brought upon you by referee reports you received. But dogmatism should be avoided. I think the suggestion I am making above is quite reasonable, elegant in writing and suggestive for teaching. I am happy to accept that you opted for a different choice, but that makes neither of these “wrong”.
What, then, do you propose to call a type operation that is neither a monad nor a comonad?
Of course a terminological choice cannot be “wrong” in a factual sense the way a proof can, but it can be wrong in a deontic sense. I think that to change a well-established terminology, in a way that would create substantial confusion, without a very good reason, is a wrong choice. If someone came along and started calling monads “functors” and comonads “cofunctors”, I think category theorists would rightly be annoyed.
We Leibnizians are still fuming that you stole ’monad’, and the Pythagoreans aren’t too happy with us.
I guess the practice of considerably changing the meaning is OK, though, like you also did with ’category’ and ’functor’. Then you can do what you like with it.
As Mike points out, one of the differences here is that philosophers are still using the word ’modality’ and ’modal operator’ to refer to things like necessity.
Given that modal logic studies “modes of truth”, ways of propositions being true, perhaps we should check that the Licata-Shulman-Riley approach is using ’mode’ appropriately. So ’necessarily’ and ’possibly’ are modes of truth. Consider our possible worlds treatment, where the -toposes associated to modes are and . Would we not then have to think of the two modes as ’invariant’ and ’world-varying’? Aren’t the philosophers’ modes talking instead about the passage back and forth between these modes, more like qualities determining (co)reflective subcategories at one of them?
In a modal treatment of alone, the two modes are often called something like “true” and “valid”, but “valid” is just a shorthand for “necessarily true”. The modality is the universal way of making a validity statement in a true mode: to say that is true is the same as to say that is valid. I think this corresponds quite appropriately to (as true, i.e. world-varying) and (as valid, i.e. invariant). As I see it, in the statement “ is necessarily true”, the philosphers’ mode “necessarily true” has to also be interpreted as an LSR mode, i.e. a category, rather than a passage between such modes, i.e. a functor/modality: the passage between modes is what allows us to convert the statement “ is necessarily true” into a statement of the form “___ is true” (which it is not already).
As for , in the -model it is obtained from a corresponding left adjoint, but I don’t think this is generally the case for alethic modalities; one shouldn’t get too addicted to that particular model. In general one would indeed need at least a third mode for , corresponding to a judgmental synonym of “possibly true”. This is apparently what Pfenning-Davies do (section 5), while Reed uses four modes (section 4.5).
What does one get if one has a ’modality’ (in some generic sense) given by an endofunctor, and then consider the free monad on it? But then presumably one could look also at the free comonad on it.
I can’t think of anything one gets other than the free (co)monad on an endofunctor…
I mean, what does one get in the sense of the ’modal types’: are things different in the three cases: endofunctor, free monad, free comonad? I just ask because it could be an argument for/against the naming issue.
I think the terminology “modal type” doesn’t really make sense except for an idempotent monad or idempotent comonad. For an endofunctor you can talk about endofunctor-algebras or -coalgebras, and for a non-idempotent (co)monad you can talk about monad-(co)algebras, and the monad-(co)algebras for an (algebraically) free (co)monad on an endofunctor coincide with the endofunctor-(co)algebras for the original endofunctor. But in a modal type theory for an endofunctor there is only one mode, and the same in a naive presentation of a modal type theory for a monad or comonad, although it’s also possible to decompose the latter into an adjoint pair of modalities between two modes. And universality relations like “this monad is the free monad on this endofunctor” can’t really be expressed in modal type theory, that I know of.
OK, thanks.
Re #25, Ok thanks. I’m getting there, but there seems to be one thing blocking me. Why should I be allowed to use the same letter across modes? If we have two nodes, and , and an adjunction, between associated categories, when a proposition in the category of validity is established, why doesn’t that concern in the category of truth? It can’t be that I use for since the latter’s not a comonad.
Or is it that we only care about the propositions in the category of validity which are , for in the category of truth? Then once is established over in the category of validity, we refer to it in ’truth’ as .
Yes, that’s confusing. In Pfenning-Davies style, all the propositions in the valid mode are of the form , and the operation is not notated.
Great, a sanity check. Thanks.
1 to 33 of 33