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 bundle bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics 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 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 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.
    • CommentAuthorMike Shulman
    • CommentTimeNov 15th 2016

    The referee of BFP in RCoHoTT complained (quite justifiably) that sometimes I call \flat 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 \lozenge and comonads like \Box 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 ,,ʃ\flat,\sharp,ʃ 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?

    • CommentRowNumber2.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 16th 2016

    Not terrible, no.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 16th 2016

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

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeNov 16th 2016

    Category theory has the advantage that an X in 𝒞\mathcal{C} is generally the same as a co-X in 𝒞 op\mathcal{C}^{op}, 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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 16th 2016
    • (edited Nov 16th 2016)

    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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeNov 16th 2016

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

    • CommentRowNumber7.
    • CommentAuthorKeithEPeterson
    • CommentTimeNov 26th 2016
    Isn't 'monad' Greek in origin? However the suffix '-al' is Latin, whereas the suffix '-ity' is from the French 'ité,' itself from from Latin '-itas', '-itatis'.

    Perhaps 'monadomorphs', though that sounds like a biological class of creatures.
    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeNov 26th 2016

    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.

    • CommentRowNumber9.
    • CommentAuthorColin Zwanziger
    • CommentTimeNov 28th 2016
    • (edited Nov 28th 2016)

    Re: #1, As you say, both \lozenge and \Box are called “modalities” in ordinary modal logic, which would seem to suggest calling both \flat and \sharp “modalities”. If you like the term “comodality”, perhaps you could introduce it explicitly as an abbreviation for “comonadic modality”?

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeNov 28th 2016

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

  1. 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 \flat. There doesn’t seem to be any reason to prefer the term “modality” for \sharp over \flat other than the fact that “monad” and “modal” sound similar.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeNov 28th 2016

    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.

    • CommentRowNumber13.
    • CommentAuthorKeithEPeterson
    • CommentTimeNov 29th 2016
    • (edited Nov 29th 2016)
    But wont that be confusing to students learning about cohesion? If it's confusing to a peer-reviewer, then students down the line are likely to be confused as well.
    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeNov 29th 2016

    Well, the specific confusing situation from #1 that the referee complained about, where \flat was sometimes called a modality and sometimes a comodality, will no longer obtain. The word “comodality” won’t be used; \flat 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.

    • CommentRowNumber15.
    • CommentAuthorKeithEPeterson
    • CommentTimeNov 29th 2016
    • (edited Nov 29th 2016)
    Oh. Okay. That's reasonable.
    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJun 15th 2018

    Late to this discussion. Just to say that I see only one way to complete the pattern.

    A\phantom{A} unit A\phantom{A} counit
    A\phantom{A} reflection A\phantom{A} coreflection
    A\phantom{A} localization A\phantom{A} A\phantom{A} colocalization A\phantom{A}
    A\phantom{A} modality AA\phantom{AA} ?!?
    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJun 15th 2018
    reflective subcategory coreflective subcategory (not cosubcategory)
    monadic functor comonadic functor (not monadic cofunctor)
    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJun 15th 2018

    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.

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeJun 16th 2018
    • (edited Jun 16th 2018)

    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?

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2018

    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. \lozenge) and to the comonadic sort (e.g. \Box).

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJun 16th 2018
    • (edited Jun 16th 2018)

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

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2018

    What, then, do you propose to call a type operation that is neither a monad nor a comonad?

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeJun 17th 2018

    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.

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 17th 2018
    • (edited Jun 17th 2018)

    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 (,1)(\infty, 1)-toposes associated to modes are H\mathbf{H} and H/W\mathbf{H}/W. 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?

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeJun 18th 2018

    In a modal treatment of \Box alone, the two modes are often called something like “true” and “valid”, but “valid” is just a shorthand for “necessarily true”. The modality \Box is the universal way of making a validity statement in a true mode: to say that A\Box A is true is the same as to say that AA is valid. I think this corresponds quite appropriately to H/W\mathbf{H}/W (as true, i.e. world-varying) and H\mathbf{H} (as valid, i.e. invariant). As I see it, in the statement “AA 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 “AA is necessarily true” into a statement of the form “___ is true” (which it is not already).

    As for \lozenge, in the H\mathbf{H}-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 \lozenge, 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).

    • CommentRowNumber26.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 18th 2018

    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.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeJun 18th 2018

    I can’t think of anything one gets other than the free (co)monad on an endofunctor…

    • CommentRowNumber28.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 18th 2018

    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.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeJun 19th 2018

    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.

    • CommentRowNumber30.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 19th 2018

    OK, thanks.

    • CommentRowNumber31.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 19th 2018
    • (edited Jun 19th 2018)

    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, tt and vv, and an adjunction, F αU αF_{\alpha} \dashv U_{\alpha} between associated categories, when AA a proposition in the category of validity is established, why doesn’t that concern F αAF_{\alpha} A in the category of truth? It can’t be that I use \Box for F αF_{\alpha} since the latter’s not a comonad.

    Or is it that we only care about the propositions in the category of validity which are U αAU_{\alpha} A, for AA in the category of truth? Then once U αAU_{\alpha} A is established over in the category of validity, we refer to it in ’truth’ as A\Box A.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeJun 19th 2018

    Yes, that’s confusing. In Pfenning-Davies style, all the propositions in the valid mode are of the form U αAU_\alpha A, and the operation U αU_\alpha is not notated.

    • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 20th 2018

    Great, a sanity check. Thanks.