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

Discussion Tag Cloud

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.
    • CommentAuthorUrs
    • CommentTimeDec 6th 2012
    • (edited Jan 5th 2013)

    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 ]

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

    etaleopenadmissibleetale\Rightarrow open \Rightarrow admissible
    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeDec 14th 2012

    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!

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

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeDec 14th 2012
    • (edited Dec 14th 2012)

    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? Πx:Π(X)Y(x)\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.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 14th 2012

    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.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeDec 14th 2012

    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\trebleclef? :-)

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 14th 2012

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

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeDec 14th 2012

    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 π n\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? (-:

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 16th 2012
    • (edited Dec 16th 2012)

    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.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 29th 2012

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

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)

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

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)

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

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)

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

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeDec 29th 2012
    • (edited Dec 29th 2012)

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

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2012

    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}$.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeDec 30th 2012
    • (edited Dec 30th 2012)

    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?

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeDec 30th 2012

    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.

    • CommentRowNumber19.
    • CommentAuthorColin Zwanziger
    • CommentTimeJun 12th 2017
    • (edited Jun 13th 2017)

    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 Π (0)\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).

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJun 13th 2017

    Urs can probably point to where and when he started using them. I think the idea was that A\flat A is the moduli space for bundles with flat AA-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.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJun 13th 2017
    • (edited Jun 14th 2017)

    Yes, I had settled or \flat early on, because BG\flat \mathbf{B}G classifies flat GG-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 X\sharp X classifies possibly discontinuous and hence “sharply varying” maps into XX.

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

    • CommentRowNumber22.
    • CommentAuthorColin Zwanziger
    • CommentTimeJun 13th 2017
    • (edited Jun 13th 2017)

    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.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJun 14th 2017
    • (edited Jun 14th 2017)

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