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

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

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

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

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

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

]]>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 ∫), 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}$`

.

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

]]>§ 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’)?

]]>Hm, 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”.

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

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

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

]]>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? (-:

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

]]>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$? :-)

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

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

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

]]>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!

]]>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$ ]]>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* ]