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 23 of 23
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 ]
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$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!
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”.
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.
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.
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$? :-)
Have you used the other musical symbol $\natural$, yet?
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? (-:
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.
Is there a common notation in shape theory for the shape of a space?
Mardešić in Thirty years of shape theory writes “$S$” for shape and “$\bar S$” for strong 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”.
§ 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’)?
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)!
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}$
.
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?
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.
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)$.
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.
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.
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.
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”.
1 to 23 of 23