Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeDec 6th 2012
   • (edited Jan 5th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexcreated little entries [[Pi modality]] $\dashv$ [[flat modality]] $\dashv$ [[sharp modality]] for completeness. The first one redirects to what used to be called _[[Pi-closed morphism]]_, but which should be generalized a bit. [edit: later we renamed the "Pi modality" to _[[shape modality]]_ ]

   created little entries

   Pi modality $\dashv$ flat modality $\dashv$ sharp modality

   for completeness. The first one redirects to what used to be called Pi-closed morphism, but which should be generalized a bit.

   [edit: later we renamed the “Pi modality” to shape modality ]

2. • CommentRowNumber2.
   • CommentAuthorStephan A Spahn
   • CommentTimeDec 6th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItexDid you check if A6 of the axioms for [[open map]]s is satisfied? If I remember correctly we have for a class of morphisms we have $$etale\Rightarrow open \Rightarrow admissible$$

   Did you check if A6 of the axioms for open maps is satisfied?

   If I remember correctly we have for a class of morphisms we have

   $$etale\Rightarrow open \Rightarrow admissible$$
3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeDec 14th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI'm sorry I haven't had the time to follow some of the recent discussions here. Just to convince you that we're not spinning our wheels, I will throw out a teaser that today we discovered a potential whole new use for $\sharp$ modalities, of direct interest to type theorists. (-: But, I have a question: is there any alternative name for $\Pi$ modalities that we could come up with? $\Pi$ is not really an available letter in type theory!

   I’m sorry I haven’t had the time to follow some of the recent discussions here. Just to convince you that we’re not spinning our wheels, I will throw out a teaser that today we discovered a potential whole new use for $\sharp$ modalities, of direct interest to type theorists. (-:

   But, I have a question: is there any alternative name for $\Pi$ modalities that we could come up with? $\Pi$ is not really an available letter in type theory!

4. • CommentRowNumber4.
   • CommentAuthorStephan A Spahn
   • CommentTimeDec 14th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItex> throw out a teaser that today we discovered a potential whole new use for ♯ modalities, of direct interest to type theorists. (-: This is really an effective teaser! Can you shortly state what it is? Another question: I had the idea of formalizing some statements on $\Pi$-closed morphisms in coq or hoq. So I looked at https://github.com/mikeshulman/HoTT/tree/master/Coq/Subcategories which works only with the mentioned patch. Do you have improved on this in the meantime to some code which just goes through in classical coq without any problem? > is there any alternative name for $\Pi$ Maybe something reminding of identity types since $\Pi$ is inspired from "path groupoid".

   throw out a teaser that today we discovered a potential whole new use for ♯ modalities, of direct interest to type theorists. (-:

   This is really an effective teaser! Can you shortly state what it is?

   Another question: I had the idea of formalizing some statements on $\Pi$-closed morphisms in coq or hoq. So I looked at https://github.com/mikeshulman/HoTT/tree/master/Coq/Subcategories which works only with the mentioned patch. Do you have improved on this in the meantime to some code which just goes through in classical coq without any problem?

   is there any alternative name for $\Pi$

   Maybe something reminding of identity types since $\Pi$ is inspired from “path groupoid”.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeDec 14th 2012
   • (edited Dec 14th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHi Mike, that's interesting news! Concerning "$\Pi$": is the problem the chance of misreading it for ``$\prod$?'' And is that such a big problem? $\Pi\underset{x \colon \Pi(X)}{\prod} Y(x)$? Otherwise, why is it more problematic than "$\flat$'" and "$\sharp$'"? I am not sure I understand.

   Hi Mike,

   that’s interesting news!

   Concerning “$\Pi$”: is the problem the chance of misreading it for “$\prod$?” And is that such a big problem? $\Pi\underset{x \colon \Pi(X)}{\prod} Y(x)$?

   Otherwise, why is it more problematic than “$\flat$’” and “$\sharp$’”? I am not sure I understand.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeDec 14th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexNo, the reflective subcategories code still requires type-in-type or universe polymorphism -- hopefully the latter will be in a version of coq available soon. And Urs, yes, that is the problem, and yes, I think it is a big problem. Can't you see how ugly and confusing that type that you just wrote down is? Note also that different type theorists use different typefaces and formatting conventions for the $\Pi$ in a dependent product, so we can't rely on any particular choice to distinguish.

   No, the reflective subcategories code still requires type-in-type or universe polymorphism – hopefully the latter will be in a version of coq available soon.

   And Urs, yes, that is the problem, and yes, I think it is a big problem. Can’t you see how ugly and confusing that type that you just wrote down is? Note also that different type theorists use different typefaces and formatting conventions for the $\Pi$ in a dependent product, so we can’t rely on any particular choice to distinguish.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeDec 14th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItex> Can’t you see If I try hard and with the right substances I can see all kinds of things :-) But if I relax, I don't see it, no. Are you sure type theory will be a pleasant foundation if it insist that the two standard symbols $\Sigma$ and $\Pi$ never be used? Maybe you are. Well, then, what can we do? "$\pi$" maybe? Or $\trebleclef$? :-)

   Can’t you see

   If I try hard and with the right substances I can see all kinds of things :-) But if I relax, I don’t see it, no.

   Are you sure type theory will be a pleasant foundation if it insist that the two standard symbols $\Sigma$ and $\Pi$ never be used? Maybe you are.

   Well, then, what can we do? “$\pi$” maybe? Or $\trebleclef$? :-)

8. • CommentRowNumber8.
   • CommentAuthorDavid_Corfield
   • CommentTimeDec 14th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexHave you used the other musical symbol $\natural$, yet?

   Have you used the other musical symbol $\natural$, yet?

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeDec 14th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't think it's a problem to use the standard symbols $\Sigma$ and $\Pi$ in other contexts, e.g. when adding up a Taylor series or something. It's just that here we are talking about defining a new operation on types, and there's already another, standard, operation on types denoted by $\Pi$. (Notating the modality in question by $\Pi$ is not really long established --- $\Pi_\infty$ is easily recognizable for spaces, at least, but it's not really commonly used, and dropping the $\infty$ is a recent and local modification.) I'd like something more "uppercase" than $\pi$ --- plus it's natural to use $\pi_n$ for the internally constructed homotopy groups in homotopy type theory, which are the categorical ones rather than the geometric one. And yes, I thought of $\natural$, but the problem with that is that it suggests something lying in between $\sharp$ and $\flat$, whereas at least from the adjoint functor situation it's rather $\flat$ that lies between $\sharp$ and $\Pi$. Maybe $\clubsuit$ (clubs) because it "smashes" a delicate geometric structure down to its purely homotopical information? (-:

   I don’t think it’s a problem to use the standard symbols $\Sigma$ and $\Pi$ in other contexts, e.g. when adding up a Taylor series or something. It’s just that here we are talking about defining a new operation on types, and there’s already another, standard, operation on types denoted by $\Pi$. (Notating the modality in question by $\Pi$ is not really long established — $\Pi_\infty$ is easily recognizable for spaces, at least, but it’s not really commonly used, and dropping the $\infty$ is a recent and local modification.)

   I’d like something more “uppercase” than $\pi$ — plus it’s natural to use $\pi_n$ for the internally constructed homotopy groups in homotopy type theory, which are the categorical ones rather than the geometric one. And yes, I thought of $\natural$, but the problem with that is that it suggests something lying in between $\sharp$ and $\flat$, whereas at least from the adjoint functor situation it’s rather $\flat$ that lies between $\sharp$ and $\Pi$.

   Maybe $\clubsuit$ (clubs) because it “smashes” a delicate geometric structure down to its purely homotopical information? (-:

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 16th 2012
    • (edited Dec 16th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexIn my personal writing I mostly use a boldface $\mathbf{\Pi}$. (The non-boldface $\Pi$ being instead the corresponding external reflector.) But I guess that doesn't help much either here. Sometimes however I write ${\vert - \vert}$ instead, because the other way to think of the fundamental $\infty$-groupoid of an $\infty$-stack is as its geometric realization.

    In my personal writing I mostly use a boldface $\mathbf{\Pi}$. (The non-boldface $\Pi$ being instead the corresponding external reflector.) But I guess that doesn’t help much either here.

    Sometimes however I write ${\vert - \vert}$ instead, because the other way to think of the fundamental $\infty$-groupoid of an $\infty$-stack is as its geometric realization.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 29th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIs there a common notation in shape theory for the shape of a space?

    Is there a common notation in shape theory for the shape of a space?

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexMardešić in _Thirty years of shape theory_ writes "$S$" for shape and "$\bar S$" for strong shape.

    Mardešić in Thirty years of shape theory writes “$S$” for shape and “$\bar S$” for strong shape.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexHm, concerning **S**hape: how about "§"? That also rhymes decently sect-flat-sharp $$ § \dashv \flat \dashv \sharp $$ On the other hand, if "sect" makes the user think "global sections" then that collides with $\flat$. But then, in LaTeX the code is \S which is just fine for "shape".

    Hm, concerning Shape: how about “§”?

    That also rhymes decently

    sect-flat-sharp
    

    $$§ \dashv \flat \dashv \sharp$$

    On the other hand, if “sect” makes the user think “global sections” then that collides with $\flat$. But then, in LaTeX the code is

    \S
    

    which is just fine for “shape”.

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex§ is a good idea, but I am worried about the conceptual/linguistic collision with 'sections'. Not only are there $\flat$ and $\sharp$ which both internalize the global sections functor $\Gamma$, also the type-theoretic dependent product that we are trying to distinguish from is a space of sections of a fibration! What about \$ (also looks sort of like an S) or ʃ (IPA for the sound 'sh')?

    § is a good idea, but I am worried about the conceptual/linguistic collision with ’sections’. Not only are there $\flat$ and $\sharp$ which both internalize the global sections functor $\Gamma$, also the type-theoretic dependent product that we are trying to distinguish from is a space of sections of a fibration!

    What about $ (also looks sort of like an S) or ʃ (IPA for the sound ’sh’)?

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, an integral sign such as ʃ would also have the advantage that it fits well with this map also having the interpretation of geometric realization (at least in the case that it in addition preserves products)!

    Ah, an integral sign such as ʃ would also have the advantage that it fits well with this map also having the interpretation of geometric realization (at least in the case that it in addition preserves products)!

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOf course, ʃ isn't actually the same as an integral sign ($\int$ or ∫), but I agree, the similarity is indeed nice. Shall we experiment with using it? For future reference, the way to type ʃ at the Forum and the nLab is `ʃ`, and it appears that the way to type it in LaTeX is with `\usepackage{tipa}` and then `\textesh` or `$\text{\textesh}$`.

    Of course, ʃ isn’t actually the same as an integral sign ($\int$ or ∫), but I agree, the similarity is indeed nice. Shall we experiment with using it?

    For future reference, the way to type ʃ at the Forum and the nLab is ʃ, and it appears that the way to type it in LaTeX is with \usepackage{tipa} and then \textesh or $\text{\textesh}$.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2012
    • (edited Dec 30th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItex> Of course, ʃ isn't actually the same as an integral sign ($\int$ or ∫) Ah, I wasn't paying attention. Now I see. Sure, yes, let's play with this. On the other hand, if the motivation is to find solutions for situations where people cannot or don't want to distinguish between "$\Pi$" and "$\prod$", wouldn't then the distinction between "ʃ" and an integral sign appear to be equally problematic?

    Of course, ʃ isn’t actually the same as an integral sign ($\int$ or ∫)

    Ah, I wasn’t paying attention. Now I see.

    Sure, yes, let’s play with this.

    On the other hand, if the motivation is to find solutions for situations where people cannot or don’t want to distinguish between “$\Pi$” and “$\prod$”, wouldn’t then the distinction between “ʃ” and an integral sign appear to be equally problematic?

18. • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWell, there's no such thing as globally unique notation. I think integrals are much less likely to appear in the same context as shape, although I suppose when one starts doing synthetic differential cohesion there may be integration involved. If you're worried about that, then \$ seems very unlikely to conflict with anything.

    Well, there’s no such thing as globally unique notation. I think integrals are much less likely to appear in the same context as shape, although I suppose when one starts doing synthetic differential cohesion there may be integration involved. If you’re worried about that, then $ seems very unlikely to conflict with anything.

19. • CommentRowNumber19.
    • CommentAuthorColin Zwanziger
    • CommentTimeJun 12th 2017
    • (edited Jun 13th 2017)
    • PermaLink
    Author: Colin Zwanziger
    Format: MarkdownItexDid the notations $\sharp$ and $\flat$ for modalities arise on the nLab? They already seem established by the start of this thread in 2012. Also, another reason not to like $\Pi$ is that it is being used for the connected components functor $\Pi_{(0)}$, and we are already observing a notational distinction between functors which induce the modalities ($\Delta, \Gamma, \nabla$), and the modalities themselves $(\flat, \sharp)$.

    Did the notations $\sharp$ and $\flat$ for modalities arise on the nLab? They already seem established by the start of this thread in 2012.

    Also, another reason not to like $\Pi$ is that it is being used for the connected components functor $\Pi_{(0)}$, and we are already observing a notational distinction between functors which induce the modalities ($\Delta, \Gamma, \nabla$), and the modalities themselves $(\flat, \sharp)$.

20. • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJun 13th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexUrs can probably point to where and when he started using them. I think the idea was that $\flat A$ is the moduli space for bundles with flat $A$-connection or something. I think they were earlier used by Awodey and Birkedal for their "logic of local geometric morphisms", but unfortunately with the reversed meaning --- although I believe Steve told me once that he agrees now that $\flat \dashv \sharp$ is the "right" order.

    Urs can probably point to where and when he started using them. I think the idea was that $\flat A$ is the moduli space for bundles with flat $A$-connection or something. I think they were earlier used by Awodey and Birkedal for their “logic of local geometric morphisms”, but unfortunately with the reversed meaning — although I believe Steve told me once that he agrees now that $\flat \dashv \sharp$ is the “right” order.

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJun 13th 2017
    • (edited Jun 14th 2017)
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, I had settled or $\flat$ early on, because $\flat \mathbf{B}G$ classifies flat $G$-connections. An early talk where I use this is the one at "Quantum Physics and Logic 2011" ([pdf](https://ncatlab.org/schreiber/files/QPL2011Schreiber.pdf)). Also some meeting in Erlangen in 2011 ([pdf](https://ncatlab.org/schreiber/files/Erlangen2011Schreiber.pdf)) That made me naturally think about using $\sharp$ for the right adjoint. First I hesitated, but then I realized that this works well, in that $\sharp X$ classifies possibly discontinuous and hence "sharply varying" maps into $X$. I learned about Awodey-Birkedal only later, probably from Mike.

    Yes, I had settled or $\flat$ early on, because $\flat \mathbf{B}G$ classifies flat $G$-connections.

    An early talk where I use this is the one at “Quantum Physics and Logic 2011” (pdf). Also some meeting in Erlangen in 2011 (pdf)

    That made me naturally think about using $\sharp$ for the right adjoint. First I hesitated, but then I realized that this works well, in that $\sharp X$ classifies possibly discontinuous and hence “sharply varying” maps into $X$.

    I learned about Awodey-Birkedal only later, probably from Mike.

22. • CommentRowNumber22.
    • CommentAuthorColin Zwanziger
    • CommentTimeJun 13th 2017
    • (edited Jun 13th 2017)
    • PermaLink
    Author: Colin Zwanziger
    Format: MarkdownItexOK, thank you guys for the info! Some of us at CMU have picked up the $\flat$/$\sharp$ notation, so good to know/be able to attribute origin.

    OK, thank you guys for the info! Some of us at CMU have picked up the $\flat$/$\sharp$ notation, so good to know/be able to attribute origin.

23. • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJun 14th 2017
    • (edited Jun 14th 2017)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI think the existence of what I later called $\sharp$ for the topos over smooth manifolds was pointed out to me by my then-colleague Dave Carchedi, after I returned to Utrecht from attending "Categories, Logic and Foundations of Physics VI" in Oxford in 2010. Right after my talk there ([video](https://www.youtube.com/watch?v=Ecxy4b-40Hk)), it so happened by coincidence that Peter Johnstone was speaking in the maths colloquium, and he was reviewing axiomatic cohesion. That's when I learned that the type of sequence of adjoint functors that I had run into already had the name "cohesion".

    I think the existence of what I later called $\sharp$ for the topos over smooth manifolds was pointed out to me by my then-colleague Dave Carchedi, after I returned to Utrecht from attending “Categories, Logic and Foundations of Physics VI” in Oxford in 2010. Right after my talk there (video), it so happened by coincidence that Peter Johnstone was speaking in the maths colloquium, and he was reviewing axiomatic cohesion. That’s when I learned that the type of sequence of adjoint functors that I had run into already had the name “cohesion”.