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 bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer 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-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 science 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.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2010

    Todd,

    you added to Yoneda lemma the sentence

    In brief, the principle is that the identity morphism id x:xxid_x: x \to x is the universal generalized element of xx. This simple principle is surprisingly pervasive throughout category theory.

    Maybe it would be good to expand on that. One might think that the universal property of a genralized element is that every other one factors through it uniquely. That this is true for the generalized element id xid_x is a tautological statement that does not need or imply the Yoneda lemma, it seems.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 19th 2010

    Yes, I was working on that, making an entry universal element (still under construction). Of course, the Yoneda lemma already verges on tautology – it just happens to be the deepest such near-tautology in mathematics (is that an exaggeration? I believe it anyway).

    The best way of understanding these things is through examples. Some will be forthcoming.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2010

    Okay, great, thanks.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 19th 2010

    Just to say why I thought of adding that cryptic sentence to the Idea of Yoneda lemma: I wanted to record in the Lab the answer I gave to Dan Lior over in this discussion. The sentence was added to create an opening for myself to create universal element, an article I’ll add more to later.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMay 19th 2010
    • (edited May 19th 2010)

    I added some hyperlinks and in particular added formal theorem/proof-environments. Have a look to see if you like it.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 19th 2010

    Looks nice, Urs – thanks.

    • CommentRowNumber7.
    • CommentAuthorEric
    • CommentTimeMay 23rd 2010
    • (edited May 23rd 2010)

    On Yoneda lemma, it says:

    The Yoneda Lemma

    Let CC be a locally small category, [C op,Set][C^{op}, Set] the category of presheaves on CC, then for all cCc \in C there is a canonical isomorphism

    [C op,Set](C(,c),X)X(c). [C^op,Set](C(-,c),X) \simeq X(c) \,.

    {}

    The left hand side seems a little notationally heavy for something that is actually simple. It’s just saying the set of natural transforms h XFh_X\to F and the set F(X)F(X) are in 1-1 correspondence. Is there a way to lighten things a little? Maybe

    Hom Psh(C)(h X,F)F(X)Hom_{Psh(C)}(h_X,F)\simeq F(X)

    ?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMay 23rd 2010

    Apparently notational heaviness is in the eye of the beholder. (-:

    I would regard Hom Psh(C)(h c,F)Hom_{Psh(C)}(h_c,F) as more notationally heavy than [C op,Set](C(,c),F)[C^{op},Set](C(-,c),F) since (1) it uses the redundant extra letters “Hom”, and it requires one to remember (2) that Psh(C)Psh(C) denotes the category of presheaves on CC, which means the functor category [C op,Set][C^{op},Set], and (3) that h ch_c denotes the representable functor represented by cc. By contrast, the notation [C op,Set][C^{op},Set] is a special case of a general notation for functor categories, and the notation C(,c)C(-,c) makes it evident what this functor does to an object cc', namely it takes it to C(c,c)C(c',c).

    • CommentRowNumber9.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010

    I agree with Eric.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2010

    Well, I agree more with Mike. And of course, my natural inclination would be to write

    Set C op(C(,c),F)F(c)Set^{C^{op}}(C(-, c), F) \cong F(c)

    but I also like [C op,Set](C(,c),F))F(c)[C^{op}, Set](C(-, c), F)) \cong F(c).

    Maybe is the placement of parentheses and brackets that is bothering Eric, or some other purely visual aspect? (Also: why does that page have \simeq instead of \cong?)

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMay 23rd 2010

    why does that page have \simeq instead of \cong?

    That’s probably me. I always use \simeq, never \cong. hm. Is this a problem?

    • CommentRowNumber12.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010
    • (edited May 23rd 2010)

    I’m a huge fan of the h Xh_X notation, which is standard in algebraic geometry.

    Also, Todd, How about the shortest and most intuitive notation: Nat(h X,F)F(X)Nat(h_X,F)\cong F(X)? For some reason, since NatNat is so specific, it’s often fine to use it without specifying which functor category you’re talking about (especially the writer probably just said something like: Let F,G be functors C->D).

    Finally, why is there so much opposition to the notation Psh(C)Psh(C) for [C op,Set][C^{op},Set] or Set C opSet^{C^{op}}? It’s no doubt easier to type and unambiguous to anyone who clicks the link on the lab page that says presheaf.

    I mean, look at how many special characters you have to type out for the other two notations:

    [C^{op},Set]
    vs.
    Set^{C^{op}}
    vs.
    Psh(C)

    It’s a category that category theorists use often enough to have given it a name. I mean, even the French use Psh (rather than Pref or Prefais, which one would expect). I don’t understand the opposition.

    @Urs: \simeq is usually used for a weaker notion of equivalence than isomorphism, which is always written as \cong.

    • CommentRowNumber13.
    • CommentAuthorEric
    • CommentTimeMay 23rd 2010

    If you are an expert in category theory and you know the Yoneda lemma like the back of your hand, then the notation

    [C op,Set](C(,c),X)X(c)[C^op,Set](C(-,c),X) \cong X(c)

    will seem completely obvious. In fact, even now that I understand what is going on, the notation seems obvious to me. But BEFORE I understood Yoneda lemma (to the minimal extent I currently do understand it), the notation was anything but obvious. It just looked like one big scary string of letters. This is sad, since the concept is so simple (and from what I hear, important).

    Any student reading Yoneda lemma will likely have a foundation in maths OR physics (OR computer science). If their foundation is physics (or CS), then Psh(C)Psh(C) is probably a little more clear than [C op,Set][C^{op},Set]. You are doing something to CC. PshPsh is the operation of taking at category CC and looking at the contravariant maps from CC to SetSet.

    If you know what a category is, then you know what a hom-set is, so Hom Psh(C)(X,Y)Hom_{Psh(C)}(X,Y) is the set of all morphisms in Psh(C)Psh(C) from XX to YY. A little checking will tell you that the morphisms in Psh(C)Psh(C) are natural transformations, so Hom Psh(C)(X,Y)Hom_{Psh(C)}(X,Y) is a set of natural transformations.

    The link to hom-functor will tell you what h Xh_X is. I think physicists will like this notation because it is very similar to tensor notation. h Xh_X is a contravariant map and h Xh^X is a covariant map. Hence hh is “like” a (1,1)-tensor, i.e. contravariant in one slot and covariant in the other with “components” h Y X=hom(X,Y)h^X_Y = hom(X,Y).

    I do not disagree with Mike’s point. The notation

    [C op,Set](C(,c),X)X(c)[C^op,Set](C(-,c),X) \cong X(c)

    is clean efficient and to the point if you already know what it means. That is common observation about the nLab. Most things are written for the sake of those who already know what everything means. It is not easy to learn from the nLab (yet). That is not a criticism because I don’t think that is necessarily what the nLab is for, i.e. it is a tool for you guys to help with your work, not necessarily to be a teaching tool for noobs like me.

    Please take my word for it. If you do not know what Yoneda lemma means, then the notation [C op,Set](C(,c),X)X(c)[C^op,Set](C(-,c),X) \cong X(c) is intimidating even though the concept is simple enough.

    The cleanest and most efficient notation is not necessarily the best for learning. Sometimes the notation can help guide the learning process. For example,

    Hom Psh(C)(h X,F)Hom_{Psh(C)}(h_X,F)

    tells you you need to know what HomHom means, you need to know what Psh(C)Psh(C) means, and you need to know what h Xh_X means. Hopefully, you know what HomHom means, so move onto PshPsh, etc.

    • CommentRowNumber14.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 23rd 2010

    Can I interject in the hom-set wars :) and remind people of the notation C^:=Set C op=Cat(C op,Set)=etc\widehat{C} := Set^{C^{op}} = Cat(C^{op},Set) = etc (sometimes even C ^C{}^\hat{} is used). I believe this is a Grothendieckian thing. Then the disputed glyph will be

    C^(c̲,F) \widehat{C}(\underline{c},F)

    where we know C^\widehat{C} is the free cocompletion of CC, and we denote an object cc of CC by c̲\underline{c} when thinking of it as an element of C^\widehat{C} i.e. the representable presheaf. Yoneda is then

    C^(c̲,F)F(c)(natural) \widehat{C}(\underline{c},F) \simeq F(c) \quad (natural)

    (on previewing: widehats seem to come out very small in Firefox. Anyone else have a problem?)

    • CommentRowNumber15.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010
    • (edited May 23rd 2010)

    Well, first of all, David, the notation you’re alluding to is literally C^C\text{^}, which appears that way all throughout EGA and SGA. It is his equivalent of Psh(C). However, Grothendieck uses honest Hom functors.

    Here is his notation for the Yoneda lemma cf. SGA 4 expose 1:

    Hom C^(h(X),F)F(X)Hom_{C\text{^}}(h(X),F)\cong F(X).

    Letter-for-letter. As I said earlier, Grothendieck used the actual written out Hom functor. I think Mac Lane invented the other notation.

    Anyway, we’ve got grothendieck on our side (because life is a contest)!

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2010

    David, I would happy with that, provided a reminder is given for C^\hat{C} and c̲\underline{c}. It’s actually somewhat Lawverean in style, and it seems to be a good compromise: no redundant HomHom, and it’s very uncluttered. +1

    Urs, in my experience, the usual symbol for isomorphism is \cong, with \simeq reserved for equivalence of categories and \sim for bi-equivalence of bicategories (and from there on up?). It could be that people are beginning to default to \simeq to take care of any level of non-evil equivalence except for 0-equivalence (equality), and I’m just old-fashioned. I don’t think it bothers me, since I only just noticed it now while we’re squabbling over notation.

    • CommentRowNumber17.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010
    • (edited May 23rd 2010)

    @Todd: h(X)h(X) or h Xh_X are 100% standard notation for representable functors. Why would we change that?

    Also, C^\hat{C} is just crappier than Psh(C)Psh(C) in every possible way. It is nonstandard (it is really only used by Moerdijk and Mac Lane, and Johnstone). I think that it’s horrible notation. I agree with Eric that notation should be suggestive of the meaning, and this has taken all of the meaning out. If people start using this combination on the lab, I intend to change it whenever I come across it.

    I’m sorry if that is considered rude, but I find that notation that bad.

    I propose the following convention: if you’re going to write it as C(x,y)C(x,y), could you replace CC with 𝒞\mathcal{C}? This breaks it up from the normal roman letters.

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2010

    Harry, having accommodated you over at operad by writing a whole bunch of PshPsh’s (which I am just about to announce at Latest Changes), just to please you and against my custom, your level of aggression regarding notation here and elsewhere is seriously pissing me off.

    If people start using this combination on the lab, I intend to change it whenever I come across it.

    Sigh.

    Listen, it wasn’t my suggestion, it was David’s. I was merely indicating willingness to go along with it, for the sake of harmony.

    • CommentRowNumber19.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010

    I really don’t like that notation, but I am not going to actually do what I said I haven’t slept now in 46 hours. Sorry if I came off like a jerk. I’m really harmless and don’t mean half of the things I say. I’ve been told that I have no “filter”.

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2010

    Yes, please get some rest now.

    I propose the following convention: if you’re going to write it as C(x,y)C(x,y), could you replace C with 𝒞\mathcal{C}?

    That’s not something I plan to do when I write pages. Sorry, but I have my reasons. If you want to do it when you write pages, that’s your prerogative.

    • CommentRowNumber21.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010

    That’s not something I plan to do when I write pages. Sorry, but I have my reasons.

    Care to elaborate? (I’m done arguing. It’s just that this intrigued me.)

    • CommentRowNumber22.
    • CommentAuthorEric
    • CommentTimeMay 23rd 2010

    I’m curious, is there any mathematician out there that doesn’t like to see op{}^{op} and prefers keeping track of covariant versus contravariant functors instead? The reason for throwing op{}^{op} all over the place seems to be so that you only need to keep track of one kind of functor. I can imagine situations where it is cleaner to not use any op{}^{op}s and just explicitly keep track of two different classes of functors instead.

    By the way, I was reading MacLane tonight and saw him write things like “contravariant functor F:C opSetF: C^{op}\to Set”, which makes me cringe a little bit (just a little) every time I see it. That is minor though. I can live with occasional cringes :)

    But as far as notation for [C op,Set][C^{op},Set] and Hom C(,X)Hom_C(-,X) is concerned, whatever choice is made, I hope it is at least sufficient to handle the related cases of [C,Set][C,Set] and Hom C(X,)Hom_C(X,-) cleanly as well. For example, I like h Xh_X for Hom C(,X)Hom_C(-,X) and h Xh^X for Hom C(X,)Hom_C(X,-). If Grothendieck uses h(X)h(X) for Hom C(,X)Hom_C(-,X), what would he use for Hom C(X,)Hom_C(X,-)?

    By the way, the feeling I get when I think about h Xh_X as “components” is too strong to ignore. Is there any real sense in which this can relate to old fashioned tensor fields (and its notation) on manifolds?

    I would like to also direct your attention to the nLab page dedicated to Notation.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2010

    I have to be in the mood to write math calligraphy; I don’t much like big fancy fonts. For one, they take longer to type. For another: very often I’ve registered the observation that mathematicians save their big fancy fonts for their biggest fanciest notions, and what that might signify is that they are themselves not totally comfortable with their notion. (I’m not saying this applies in the present circumstance.) I picked up this idea from Ross Street, who counteracts this tendency by writing something like ’ee’ for a hypercover in a topos, and I have a liking for the freedom from enthrallment to notation that this implies, even if I don’t go so far as Ross does sometimes.

    Third, regarding the present circumstance, it’s the same category CC that’s meant to be referred to, so I see no reason to change the font – that I would find confusing if I were reading it. Those are some intellectual arguments I can give. There may be emotional components as well at this stage of the discussion.

    • CommentRowNumber24.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010

    Third, regarding the present circumstance, it’s the same category that’s meant to be referred to, so I see no reason to change the font – that I would find confusing if I were reading it. Those are some intellectual arguments I can give. There may be emotional components as well at this stage of the discussion.

    Ah, well if that’s how it came out, that must’ve seemed pretty stupid. I was saying that you should just use calligraphy (or boldface) for all one-letter categories when you write your Hom-sets as C(X,Y). This makes it easier to tell what’s a category and what’s a functor or an object in long written expressions.

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 23rd 2010
    • (edited May 23rd 2010)

    I didn’t know about the Notation page. That’s nice.

    I’m curious, is there any mathematician out there that doesn’t like to see op ^op and prefers keeping track of covariant versus contravariant functors instead?

    It’s sometimes done, and I guess used to be done more. It has a kind of old-fashioned feel to me.

    I was reading MacLane tonight and saw him write things like “contravariant functor F:C opSetF: C^{op} \to Set”, which makes me cringe a little bit (just a little) every time I see it.

    That’s understandable; it’s sort of like a double negative. In some languages (such as Russian, I’m told) and colloquial English, double negatives may signify no’s with greater emphasis, and I think that’s more or less the same function here. It may seem a little odd in the more formal language of mathematics, but it doesn’t bother me much if at all. I may be guilty of sometimes doing that myself.

    @Harry: I still disagree, but basta.

    • CommentRowNumber26.
    • CommentAuthorEric
    • CommentTimeMay 23rd 2010

    I’m curious, is there any mathematician out there that doesn’t like to see op ^op and prefers keeping track of covariant versus contravariant functors instead?

    It’s sometimes done, and I guess used to be done more. It has a kind of old-fashioned feel to me.

    If you or anyone can think of an example reference, I’d be curious to have a look. I’d like to know the motivation if only out of curiosity.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeMay 23rd 2010

    I think \cong is still generally used for isomorphism, but \simeq is used for all sorts of equivalence weaker than this. In particular \simeq is commonly used for weak equivalences in homotopy theory, which can be yet weaker than biequivalences. I’d rather not use \sim for any of these; to me that symbol looks too “flimsy” to have such a meaning. (-:

    It’s a category that category theorists use often enough to have given it a name.

    It has a name: [C op,Set][C^{op},Set] or Set C opSet^{C^{op}}. I much prefer having general rules for notation, such as “this is the notation for a functor category,” and then whenever you see a functor category, you use that notation for it, rather than inventing new notations for particular functor categories all the time. I find that when people invent new notations for things that are special cases of existing more general notations, it makes their papers harder to read, and in particular harder to skim: if I open up the paper in the middle and see notation I don’t know, I have to search backwards until I find the definition of that notation. The notation “Psh” is common enough that I, personally, have learned what it means by now, but on general principles I still think it is better to use general notation. I feel the same way about C^\widehat{C} and C C^\wedge.

    That isn’t to say that I haven’t used these shorter notations myself sometimes, locally, but I generally try to to remind the reader of what that notation means at the beginning of any discussion that uses it. My comment #8 was intentionally somewhat overstated to make a point; I don’t object strongly to these notations but I think it is always better to say what they mean when you use them.

    BTW, Harry, I think you’re wrong about the (non)standardness of C^\widehat{C}; I’ve seen it in numerous other papers.

    The choice of script letters versus roman letters is something where I think we should also respect the authors of individual pages and maintain consistency with what’s already written. I tend to use script letters much less in the nLab than I do in ordinary papers, for two main reasons: (1) on the nLab I have to write out \mathcal{C} instead of being able to define a macro \sC, and I’m lazy, and (2) script letters may not display well for people who don’t have math fonts installed.

    Also I think that using different fonts is most helpful when there are a lot of different kinds of things floating around, so that fonts can help distinguish them; I often use a convention like boldface roman capitals = categories, script capitals = 2-categories, blackboard bold = double categories, roman capitals = objects of categories, roman lower case = morphisms in categories, greek lower case = 2-cells in categories. I find this very helpful myself. But few nLab pages are long enough for that to be worthwhile, I think.

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeMay 23rd 2010

    Re: contravariance, I expressed my opinion here.

    • CommentRowNumber29.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 23rd 2010

    Also I think that using different fonts is most helpful when there are a lot of different kinds of things floating around, so that fonts can help distinguish them; I often use a convention like boldface roman capitals = categories, script capitals = 2-categories, blackboard bold = double categories, roman capitals = objects of categories, roman lower case = morphisms in categories, greek lower case = 2-cells in categories. I find this very helpful myself. But few nLab pages are long enough for that to be worthwhile, I think.

    Too late, I like this convention, so now I’ll be saying “let’s adopt Mike’s convention”.

    =D!

    BTW, Harry, I think you’re wrong about the (non)standardness of C^\hat{C} ; I’ve seen it in numerous other papers.

    We should ask Urs to ask Moerdijk if C^\hat{C} is a bastardization of C C^{\wedge} or if it’s the other way around.

    • CommentRowNumber30.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 24th 2010

    I meant to write something like C C^{\wedge}, but couldn’t figure it out at the time. I prefer it to C^\widehat{C}, as that could just be something along the lines of “take categories CC and C^\widehat{C}…”

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeMay 24th 2010
    • (edited May 24th 2010)

    I don’t quite have the time to follow this discussion, but would just briefly like to make one point:

    the nLab is not supposed to be a gauge for canonicity, but a place where things are explained. If it happens, as it does here, that there is one notation preferred by practitoners, but another notation better suited to introduce the subject to newcomers to the field (by the own account of these newcomers), then by all means the entry should say so and explain both notations somewhere at the beginning.

    • CommentRowNumber32.
    • CommentAuthorEric
    • CommentTimeMay 24th 2010

    Sounds good. We could even have a pseudo notation

    Set of Natural Transformationsh XFF(X)\text{Set of Natural Transformations}\; h_X \to F \cong F(X)
    • CommentRowNumber33.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 24th 2010
    • (edited May 24th 2010)

    @Eric: That is exactly what

    Nat(h X,F)F(X)Nat(h_X,F)\cong F(X)

    means. As I was saying earlier, this is the notation that gives the proper interpretation.

    Also, the explanation for why Grothendieck uses h(X)h(X) rather than h Xh_X is that h(X)h(X) is actually for h 𝒰(X)h_\mathcal{U}(X) for some universe 𝒰\mathcal{U} with the universe suppressed.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeMay 24th 2010
    • (edited May 24th 2010)

    That is exactly what Nat(h X,F)F(X)Nat(h_X,F)\cong F(X) means.

    Er. It’s also exactly what [C op,Set](C(,X),F)[C^{op}, Set](C(-,X), F) means! ;-)

    As I was saying earlier, this is the notation that gives the proper interpretation.

    Somehow this remark is missing a point…

    Anyway, I now went ahead and edited the paragraph to reflect the discussion here a little. See Yoneda lemma – Statement of the lemma

    • CommentRowNumber35.
    • CommentAuthorHarry Gindi
    • CommentTimeMay 24th 2010

    s/interpretation/intuition/

  1. Could someone explain what the intended meaning of the original sentence under discussion is?

    "In brief, the principle is that the identity morphism
    idx:x→x is the universal generalized element of x. This simple principle is surprisingly pervasive throughout category theory."

    Urs suggests it is not the fact that the identity is a universal element of Hom(X,-).

    It sounds like the above quotation is pointing towards some nice way to connect Yoneda to the fact that the identity can distinguish maps?


    (Relatedly I have seen several times online someone saying that the "meaning" of the Yoneda lemma is that "if you know how it interacts with everything, then you know what it is up to isomorphism", but unless I am missing something (and please tell me if I am), this seems like a bit of a swindle, because the proof relies not on the input of precomposition with anything, but only on a fact about the identity. Also, it tells us "if you know how it interacts with everything on one side, you know everything up to is", so we don't even need to know everything about its interactions)
    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeMar 24th 2014
    • (edited Mar 24th 2014)

    Hi,

    the above is a fairly ancient discussion, I forget what I was trying to make Todd do back then! :-)

    Of course in the proof of the Yoneda lemma one ends up looking at all generalized elements of the representing object (which appear as the components in the domain of the natural transformation into the given presheaf) and observes that they all factor uniquely through the universal one, concluding that hence the component of that natural transformation is fixed on all components once it is fixed on the universal one.

    I’d think what the entry needs is not more heavy language, but maybe just more details on how this simple proof works. Recently I pointed a young student to the page and realized that just displaying that naturality diagram would help newcomers see, as it should be, that that which is trivial is trivially trivial ;-)

    Maybe somebody here has the time and energy to draw the relevant naturality diagram and add it to the entry, for better illustration of the proof?

    • CommentRowNumber38.
    • CommentAuthorZhen Lin
    • CommentTimeMar 24th 2014

    It is the universal element of Hom(X,)Hom (X, -), in the sense of representing the functor FF(X)F \mapsto F (X).

    • CommentRowNumber39.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 24th 2014
    • (edited Mar 24th 2014)

    I would be happy to remove the offending phrase, as I’m not really inclined to spend much time defending it. :-)

    Edit: done.

    • CommentRowNumber40.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 25th 2014
    • (edited Mar 25th 2014)

    By the way, Urs, I inserted the desired diagram (at Yoneda lemma). The proof now has some redundancy in it; please feel free to trim out the redundancy.

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeMar 25th 2014

    Thanks!

    • CommentRowNumber42.
    • CommentAuthorTim_Porter
    • CommentTimeNov 11th 2014

    Someone tried to turn Yoneda lemma into a slide show (and failed!). I have rolled back one stage.

    • CommentRowNumber43.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 5th 2016
    • (edited Oct 5th 2016)

    I have added to Yoneda lemma#necessity_of_naturality a couple of examples illustrating the necessity of naturality. I came up with these in reply to the question of Michael Barr on the category theory mailing list today. It took me a few goes to get the finite example right, as you’ll see if my messages pass the moderation!

  2. Amusingly, at least three other people came up with exactly the same infinite example. Funny how the mind works (I at least certainly just came up with it from scratch)! I think the finite example I gave is minimal; I haven’t checked whether it is the same as the one Eduardo Dubuc gave (or whether his is correct).

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeJun 3rd 2018
    • (edited Jun 3rd 2018)

    I have edited a little to streamline the formatting. Merged the subsection “Preliminaries” and “The Yoneda lemma” into a single section “Statement and proof”, instead gave the “preliminaries” a numbered Definiton-environment. Removed two puny “Remark”-subsubsections which both made the same remark about generalized spaces, that is better had at Yoneda embedding.

    diff, v57, current

    • CommentRowNumber46.
    • CommentAuthorThomas Holder
    • CommentTimeJun 5th 2018

    I added some links and mentioned what happens to the Yoneda lemma in a semicategory.

    diff, v58, current

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2018

    added some hyperlinks and punctuations. Trimmed down hyperlink code of the form

     [[SingularX|PluralX]]]
    

    to

     [[PluralX]]]
    

    and instead made sure that all entries have their plural title version as a redirect.

    diff, v59, current

    • CommentRowNumber48.
    • CommentAuthorThomas Holder
    • CommentTimeJun 5th 2018
    • (edited Jun 5th 2018)

    Actually, I avoid the redirects intentionally since I don’t like the way pages are displayed when opened by a redirect. Maybe one (Richard, sorry!) could suppress the ’redirected from..’ messages at least with these plural-singular redirects and purely orthographic redirects like capitals, hyphens etc. or create a second version of the redirect command that does not display the messages !?

    I also suppose that putting in ’[[A|B]]’ is a bit more efficient than letting the engine search through all redirects looking for B , is it not !?

    • CommentRowNumber49.
    • CommentAuthorUrs
    • CommentTimeJun 5th 2018

    Okay, sorry, I see. I was thinking that it makes the source easier to read.

    • CommentRowNumber50.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    I agree with Urs. Suppressing the redirection message for purely orthographic and plural/singular redirects is a nice idea, if we can think of a good way to do it, but until then I think it’s better to live with the redirect message. Or we could perhaps make the redirection message less obtrusive in all cases.

  3. Thanks for adding this to the TODO list, Mike! I suggest that we not try to guess plural forms of words, and instead add something to the syntax when writing a redirect to indicate this. We could have

    redirect plural

    or something like that. Not sure how to do it in general. Could have

    redirect orthographic

    or

    orthographic redirect

    or something, maybe. Just let me know what you’d prefer.

    • CommentRowNumber52.
    • CommentAuthorMike Shulman
    • CommentTimeJun 8th 2018

    That was my first thought too. However, then I realized that if we did it that way then it would not take effect on any existing nLab pages unless someone went through manually, looked at all the redirects, and changed the syntax of the appropriate ones. I doubt that anyone wants to do that.

    Rather than trying to guess plural forms, what about just suppressing the redirection message whenever the page title and redirected name are “close” in some heuristic distance? We don’t have to be exact here; it’s not the end of the world if a few plural/orthographic redirects get the hatnote and a few non-orthographic ones don’t. E.g. the maximum over all “words” of the number of changed/inserted/deleted letters in that word has to be 3\le 3. (The cutoff can’t be less than 3 if we want to catch “category \to categories”, and I can’t think of a reason to make it any larger than 3.) We could also add in manually a few changes that are declared to be distance-1, such as “infinity \to ∞”.

    • CommentRowNumber53.
    • CommentAuthorThomas Holder
    • CommentTimeJun 8th 2018
    • (edited Jun 8th 2018)

    I don’t think that both strategies are exclusive. To a have redirect*- command pemits fine-tuning, is computationally cheap and a useful option for future edits and the star is easily apppended while editing an already existing page.

    In my experience plural “s”, hyphens and initial capitals are the most frequent redirects that occur in practice and just having rules for them is already a huge improvement. Using error correction would be cool to catch typos and would even make the written redirects obsolete but I see potential problems with the computational load and short names like Cat etc. though I don’t know how serious this would be.

  4. Minor inconsistency: The Yoneda functor starts as lower case yy and later morphs into upper case YY. I had to go back and convince myself that it’s the same functor.

  5. Thanks for raising, Bartosz! Good idea to make it consistent. Would you like to edit the page to do so?

    • CommentRowNumber56.
    • CommentAuthorUrs
    • CommentTimeApr 5th 2019

    fixed it

    diff, v61, current

  6. Thanks!

    • CommentRowNumber58.
    • CommentAuthorIngoBlechschmidt
    • CommentTimeApr 6th 2019
    • (edited Apr 6th 2019)

    Recently I see more and more the kana “よ” (“Yo”) used for the Yoneda embedding. It looks slightly unusual, but I guess I quite like it, because unlike the common alternatives yy, YY and hh, it doesn’t collide with those otherwise-occurring symbols. (For instance, I’d like my second object of consideration after XX to be YY.)

    Is there a general opinion on this new option?

    • CommentRowNumber59.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 6th 2019

    I prefer yy. I’ve never had a conflict (typically I would apply it to an object cOb(C)c \in Ob(C), i.e., with a name nearer the beginning of the alphabet).

    On purely aesthetic grounds I might come one day to like it, but it would be annoying to have to hunt down each time how to typeset it, whether via html or copy-and-paste.

    • CommentRowNumber60.
    • CommentAuthorMike Shulman
    • CommentTimeApr 7th 2019

    This is the first I’ve heard of this usage. Can you give some references? I admit to never having been completely satisfied with yy for the reasons mentioned; usually I choose y\mathbf{y} or 𝔶\mathfrak{y} or sometimes YY. But I’m not sure about introducing a totally new alphabet into mathematics.

    In LaTeX of course one could just define an appropriate macro \yo, and on the nLab/nForum we could add a simple command to our parser, so in these contexts we wouldn’t have to keep hunting down how to type it (though in other web contexts like mathoverflow that use vanilla mathjax the problem would remain).

    • CommentRowNumber61.
    • CommentAuthorRodMcGuire
    • CommentTimeApr 7th 2019

    Recently I see more and more the kana “よ” (“Yo”) used for the Yoneda embedding.

    Most mathematicians (except mostly native readers) don’t know hiragana. As is the case for Cyrillic, Hebrew and other scripts. (but they do know the Latin and Greek scripts)

    The problem with using an unknown script is you can’t recognize the characters and instantly be able to tell that two characters in that script are different without visually comparing them.

    Sure one could make a unique exception for “よ”, similar to how \aleph is the only Hebrew letter used in math. (the rule being if it looks Japanese it is “yo” while if looking Hebrew its “aleph”). If you open the floodgates to more characters in these scripts then you run into the recognizably problem.

    • CommentRowNumber62.
    • CommentAuthorMike Shulman
    • CommentTimeApr 7th 2019

    \aleph isn’t the only Hebrew letter used in math. It’s probably the most commonly recognized one, but \beth is also used in cardinal arithmetic: wikipedia.

    I think the problem of distinguishability only arises if you use characters that look similar. I don’t know the Hebrew script but I don’t have any trouble telling the difference between \aleph and \beth. By contrast, the latex symbols list also includes a \gimel that I would have a very hard time telling apart from \beth. (And a \daleth that is probably sufficiently distinct.)

    The problem of distinguishability doesn’t only arise with different alphabets, but even with different fonts sometimes. I have a very hard time telling \mathfrak{C} apart from 𝔈\mathfrak{E}.

  7. @Mike 60: I first stumbled on this usage in:

    • Emily Riehl, Dominic Verity. Elements of \infty-category theory. web (attributing the suggestion to Doug Ravenel)

    Other references include (in no particular order):

    • David Li-Bland. The stack of higher internal categories and stacks of iterated spans. arXiv:1506.08870 (attributing the suggestion to Theodore Johnson-Freyd)
    • Fosco Loregian. This is the (co)end, my only (co)friend. arXiv:1501.02503 (attributing the suggestion to the previously-listed paper)
    • Michael Hill, Michael Hopkins, Douglas Ravenel. Equivariant stable homotopy theory and the Kervaire invariant problem. web (attributing the suggestion to Eric Peterson)

    LaTeX code for producing the symbol is:

    % lifted from https://arxiv.org/abs/1506.08870
    \DeclareFontFamily{U}{min}{}
    \DeclareFontShape{U}{min}{m}{n}{<-> udmj30}{}
    \newcommand\yon{\!\text{\usefont{U}{min}{m}{n}\symbol{'210}}\!}
    
    • CommentRowNumber64.
    • CommentAuthorMike Shulman
    • CommentTimeApr 9th 2019

    Thanks. That’s a very curious collection of conflicting attributions!

    I think I could probably get used to よ. It would be nice to have a clearly distinguished symbol for such an important object.

    • CommentRowNumber65.
    • CommentAuthorMike Shulman
    • CommentTimeApr 9th 2019

    Curious that they defined the command to be \yon rather than \yo

    • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeApr 9th 2019

    By the way, for those of us without a Japanese keyboard, よ can be produced on the web (without copy-paste) by &#x3088;.

    (BTW, according to Wikipedia, the katakana version of the same kana is ヨ, which would of course be a terrible choice to use for anything in mathematics!)

    • CommentRowNumber67.
    • CommentAuthorMike Shulman
    • CommentTimeApr 12th 2019

    Theo points me to

    • Theo Johnson-Freyd, Claudia Scheimbauer. (Op)lax natural transformations, twisted quantum field theories, and “even higher” Morita categories. arxiv:1502.06526

    which is an earlier reference than any of the others.

    • CommentRowNumber68.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 12th 2019

    I guess the arXiv dates are not a perfect guide to online release date then!

    • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeApr 12th 2019

    Well, in general no, but in this case the point is to look at arXiv revisions. The use of よ doesn’t appear until v3 of the Loregian paper, posted in Jan 2017.

  8. Add a reference.

    Simon Burton

    diff, v64, current

    • CommentRowNumber71.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 23rd 2019

    Added link to authors’ copy of (Reyes–Reyes–Zolfaghari 2004).

    diff, v65, current

    • CommentRowNumber72.
    • CommentAuthorMike Shulman
    • CommentTimeMay 19th 2019

    Just a note about this from #63:

    % lifted from https://arxiv.org/abs/1506.08870
    \DeclareFontFamily{U}{min}{}
    \DeclareFontShape{U}{min}{m}{n}{<-> udmj30}{}
    \newcommand\yon{\!\text{\usefont{U}{min}{m}{n}\symbol{'210}}\!}
    

    to possibly save others some searching: in Ubuntu, the necessary font is available in the package latex-cjk-japanese.

    • CommentRowNumber73.
    • CommentAuthorMike Shulman
    • CommentTimeJul 6th 2019

    Just thought I would add a note here that よ for the Yoneda embedding follows a bit in the footsteps of the use of Cyrillic Ш (“sha”) for the Tate-Shafarevich group. Apparently Ш is also sometimes used for the Dirac comb (although Wikipedia sticks to the ASCII-art version IIIIII) and its lowercase version was the origin of the symbol ⧢ for the shuffle product.

    I wonder whether we should have considered Ш instead of ʃ for the shape modality. (Or did we? I can’t remember.)

    • CommentRowNumber74.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2019

    I like that the “esh” symbol, while being different from an integral sign, is still reminiscent of one, since this matches well with the understsnding of shape as geometric realization. Therefore I would still prefer it over “sha”.

    • CommentRowNumber75.
    • CommentAuthorMike Shulman
    • CommentTimeJul 6th 2019

    Yes, and I don’t think it would be a good idea to try to change the notation now, even if we thought that Ш was better (which I don’t either). It just occurred to me by-the-way that “sha” could also stand for “shape”.

    Maybe if we ever encounter another shape-like modality we should consider Ш for it.

    • CommentRowNumber76.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 6th 2019

    I like that the “esh” symbol, while being different from an integral sign,

    I always thought that this symbol is the integral sign. It certainly does not look different when typeset on the nLab pages.

    • CommentRowNumber77.
    • CommentAuthorMike Shulman
    • CommentTimeJul 7th 2019

    It doesn’t look very different, but I can tell the difference when they are typeset side by side: ʃ vs \int.

    • CommentRowNumber78.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 8th 2019

    This probably depends on the font. In some fonts it seems to look essentially the same.

    • CommentRowNumber79.
    • CommentAuthorMike Shulman
    • CommentTimeJul 8th 2019

    But don’t we choose the font in which the nlab is displayed, so that it should be the same for everyone? I remember a long discussion recently about what that font should be.

    • CommentRowNumber80.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 8th 2019
    • (edited Jul 8th 2019)

    Well, what if the chosen font is not available on user’s system? Then a different font is substituted.

    The chosen font for formulas currently appears to be DejaVu Serif followed by Cambria. If these two fonts are not available, then whatever font exists on user’s system is substituted.

    This could be avoided by actually loading the font files in the CSS, but currently we do this only for STIX fonts.

    • CommentRowNumber81.
    • CommentAuthorMike Shulman
    • CommentTimeJul 8th 2019

    Are you saying you don’t have those fonts available and that’s why they don’t look different for you?

    • CommentRowNumber82.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 9th 2019

    I do have DejaVu fonts installed now, but this was a separate step that I had to do, and a lot of Linux users don’t have them installed.

  9. The Stix fonts are embedded for exactly this reason, to serve as a backup. Is the problem that the two symbols look the same in Stix? Should we embed something else?

    • CommentRowNumber84.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 9th 2019

    No, the problem was that if a user does not have DejaVu Sans or Cambria installed, then formulas will use whatever sans serif font is installed, which need not distinguish between esh and integral.

    Concerning STIX: I suggest that we switch to the improved XITS fonts: https://en.wikipedia.org/wiki/XITS_font_project

    • CommentRowNumber85.
    • CommentAuthorFosco
    • CommentTimeJul 9th 2019
    • (edited Jul 9th 2019)

    Most mathematicians (except mostly native readers) don’t know hiragana.

    Sure, they don’t. Perhaps because they are never exposed to it :-)

    Mathematical notation is one of my pet-peeves (those of you who know me in person, or worse, those of you who read one of my papers, might have noticed it…), but with the passing of time this idiosyncrasy acquired a deeper meaning.

    We name things so that they can be distinguished: I see no point in trying to economize in this respect, as if names were subject to exhaustion. But it is even more a nuisance that mathematical symbols are very often overloaded with meaning (“normal”, “nice”, “admissible”, “good”, …). However, that’s not my point here.

    I chose to use the hiragana よ for the Yoneda embedding essentially because there was a precedent in this respect, but all the more because Yoneda was Japanese. But there’s a deeper reason behind this and similar choices.[¹]

    Do you ever wonder, in doing Mathematics, to what extent the ideology that permeates it (like in every other product of the human intellect, Mathematics has an ideology) is centered in Latin/Germanic cultures? I often do, and at the same time I wonder what I can do to balance this trend. Human culture is wide and rich: we have built a word for basically any concept, provided we search far enough from our home culture.

    Thus, to me, using Georgian, cuneiform, hiragana, Hebrew and Sanskrit alphabets is a precise “political” choice (that’s a heavy word, I guess, but I can’t find a better one): when I need to denote something exotic, or when I need syntax to convey a certain “flavour” together with semantics, I sometimes find restrictive to limit to Latin and Greek alphabet.

    Maybe, notation is a different matter, but I feel I’m not the only one having this peculiar ésprit, especially among category theorists :-) when we study topos theory, we sketch an elephant and not a squid, because of an old Jain tale about five (four? six?) blind men touching an animal (=a category) that resembles a tree, a throne, a fan… according to the side where you approach it from. So are toposes! You can only grasp their true nature if you approach them from every side at once. And the methaphor is borrowed from Indian culture, because Western philosophy doesn’t contain a concept similar to Jain anekanta (more or less, “manifoldness of thought”).

    ===

    [¹] See e.g. recollements or yosegi.

    • CommentRowNumber86.
    • CommentAuthorRichard Williamson
    • CommentTimeJul 9th 2019
    • (edited Jul 9th 2019)

    Re #84: That should not be possible for displayed mathematics. The embedded Stix font should be used if the other two are not found. If you see other behaviour, please post a screenshot from something like F12 in Chromium which shows which font is used.

    • CommentRowNumber87.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 9th 2019

    Here is what Firefox shows for the first displayed formula in the Yoneda lemma article as the applied CSS style:

    body { font-family: “dejavu serif”,cambria,Serif !important; }

    This comes from the beginning of the nlab.css file.

    So if DejaVu Sans or Cambria are installed, they will be used, otherwise, the generic serif font will be used.

    The style specified for the math element, which includes STIX fonts, simply does not apply here, because it specifies @media max-width: 960px, but my screen width is 3840 pixels.

  10. Thanks very much! Good catch regarding max width, that seems like it would explain it. I’ll investigate that when back from holiday.

    • CommentRowNumber89.
    • CommentAuthoratmacen
    • CommentTimeJul 10th 2019
    I’m puzzled by #87, #88. My browser window is wider than 960px (as I would guess most people’s are), but I’m not getting this effect; the formulas use STIX for me.
  11. I actually do not know anything about this @media gadget! Of course I will look it up, but respecting it might be browser dependent. Which browser were you using, Matt? I think when experimenting in the past I have always got the Stix fonts as well.

    • CommentRowNumber91.
    • CommentAuthoratmacen
    • CommentTimeJul 10th 2019

    Firefox. W3Schools said Firefox has supported @media since 3.5.

    I’m no web dev hotshot, but I wonder if Dmitri misread nlab.css. (Or maybe it’s been changed already?) Here’s the part using @media:

    @media only screen and (max-width:960px){
        .navigation:not(.navfoot){top:60px}
        h1#pageName{margin-top:100px}
    }

    So it doesn’t look like this should affect loading or use of STIX.

    • CommentRowNumber92.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 11th 2019
    • (edited Jul 11th 2019)

    Re #91: This is correct, I misread it.

    However, the rule

    math {
      font-family:dejavu math tex gyre,cambria math,stix two math!important;
      font-size:19px
    }
    

    in nlab.css somehow does not apply anyway, and the rule that I pointed above applies instead.

    This is revealed by Firefox’s inspection tools.

  12. I am still confused, Dmitri, because it would seem that the styling for body rather than math is being used, which seems unlikely, especially since Matt does not see this, and I have not previously observed it either when testing in Firefox.

    • CommentRowNumber94.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 12th 2019
    Re #93: I ran a copy of Firefox with a blank profile,
    pointed the mouse to the word "Set" in the first displayed formula,
    and copy-pasted the applied CSS style from the CSS inspector.
    Here is the result, only the first font-family is applied, the second one is ignored:

    .maruku-equation {
    font-size: 19px;
    }
    .maruku-equation {
    text-align: center;
    }
    body {
    font-family: "dejavu serif",cambria,Serif !important;
    }
    body {
    color: #333;
    font-family: noto sans,Roboto,lucida grande,san francisco,sans-serif;
    font-size: 1em;
    line-height: 1.3em;
    }
    #Content {
    text-align: left;
    }
    #Container {
    text-align: center;
    }
    • CommentRowNumber95.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 12th 2019
    Although perhaps I may be misinterpreting what Firefox says here.
    Another inspector tab shows "dejavu math tex gyre" as a font.
    • CommentRowNumber96.
    • CommentAuthoratmacen
    • CommentTimeJul 12th 2019

    Re #94: Yes, I see that too, in the “Rules” inspector tab. I don’t know why it doesn’t show the math rules. But it does show them in the “Computed” tab. Also, when I uncheck the body font family rule (in “Rules”), body text changes, but not formulas.

  13. Great, then I think the issue may after all be that the two symbols are too similar in Stix. I can verify that when back from holiday.

    • CommentRowNumber98.
    • CommentAuthorJonasFrey
    • CommentTimeMar 19th 2020

    Regarding the ubuntu package (#72): for me it only worked after I also installed “latex-cjk-japanese-wadalab”. This package is ’recommended’ by the package “latex-cjk-japanese” that Mike mentioned, but depending on your configuration recommended packages might not be automatically installed.

  14. I added a link to Emily Riehl’s book “Category Theory in Context”. Chapter 2. Universal Properties, Representability, and the Yoneda Lemma. I treasure her exposition.

    diff, v69, current

    • CommentRowNumber100.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 2nd 2021

    Added a reference to

    • Louis Martini, Yoneda’s lemma for internal higher categories, (arXiv:2103.17141)

    diff, v71, current