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-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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 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).

nLab > Latest Changes: Names of objects and universes

Bottom of Page

1 to 32 of 32

  1.  
    • CommentRowNumber1.
    • CommentAuthorMichael_Bachtold
    • CommentTimeApr 30th 2015
    • (edited Apr 30th 2015)

    Prompted by this discussion, I added a minimal explanation of the terminology “name of an object” to the page universe in a topos, right below the first diagram. Please feel free to correct if this is not right.

    Since there are several pages talking about universes I also don’t know if that’s the best place for that edit.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2015

    Thanks!

    That made me go to object classifier in an (infinity,1)-topos and edit the first paragraph of the Definition section a little.

    Gee, that entry was in a pitiful state. And still is. Where is people energetic about making available nice polished little expositions in nLab entries?

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 30th 2015

    It all has to do with available time, energy, current interests, etc. etc. I love to do it myself, when I have some time and the mood strikes. (But you know all this.)

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeApr 30th 2015

    I find myself having a lot less time for editing the nLab these days than I used to, for some reason…

    • CommentRowNumber5.
    • CommentAuthorMichael_Bachtold
    • CommentTimeMay 1st 2015
    • (edited May 1st 2015)

    Some follow-up questions: in universe in a topos, the universal arrow E→UE \to U is denoted with elel. What does elel abbreviate?

    A similar notation ElEl appears in type+of+types under Universe à la Tarski, but I’m not sure it denotes the same thing. Does it?

    Finally in object classifier in an (infinity,1)-topos, no particular name is given to the arrow Type^→Type\widehat{Type} \to Type.

    So, is there a standard (ideally suggestive) name for that arrow? How about for the domain of it? And would it be fair to call the whole thing E→UE \to U the “universal family of objects”?

    Then in the previous thread Urs made the following remark:

    If you feel idealistic, you might call ′P′ the inner reflection of the outer P.

    I was not sure if “reflection” here has a technical meaning (as e.g. in reflective+subcategory), or was it meant informally? Also in type+of+types, again under Universe à la Tarski, I read:

    …with the usual rules for the relative reflection el(a):U′ for any a:U, a choice of weakly or strongly a la Tarski computational rules for the reflections El and El′…

    but from that page I could not figure out what reflection means (in that context).

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 1st 2015

    The elel would stand for elements. You can think of this as akin to the fibration el:1↓Set→Setel: 1 \downarrow Set \to Set which projects a pointed set down to its underlying set.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2015

    Here “reflection” refers to the fact that the type universe/object classifier “reflects” the entire topos inside itself, in that it is a small “image” of the full topos inside itself. This is a different technical use of the natural language word “reflect” than in “reflective subcategory”.

    I think this is fairly standard, though we should collect references that say it that way. One that I have at hand right now is this.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2015

    I have looked up a few more authors that speak about type universes as “reflections” of the ambient type system, here.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2015
    • (edited May 1st 2015)

    Luo 11, section 2.5:

    Introducing universes can be considered as a reflection principle: such a universe reflects those types whose names are its objects.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMay 1st 2015

    Interesting, I haven’t really noticed that usage of “reflect” before. I have heard it used in the “reflection principle” of set theory, which is related but different.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2015
    • (edited May 1st 2015)

    It was already observed in 1812 that the essence appears reflected in itself, but it took a while for people to redicover this. ;-)

    BTW, in case we overlapped, I think Luo11 in #9 has it most explicitly, also the Stanf. Enc. Phil. here is pretty good:

    Adding a universe is a reflection process

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2015

    I gave reflection principle a stub. Is it sensible to list it in the list at foundational axiom?

    • CommentRowNumber13.
    • CommentAuthorThomas Holder
    • CommentTimeMay 1st 2015
    • (edited May 4th 2015)

    Martin-Löf purloins the name ’reflection principle’ for his introduction of universes in the 1973 paper ’An intuitionistic theory of types’ (reprinted in the 1995 Venice proceedings). He attributes the idea to adopt the set-theoretic reflection principle for foundations of category theory to Kreisel 1965 and Feferman 1969 (LNM 106). By the way, the ML paper also contains an embedding of intuitionistic predicate logic into TT, I think this came up on another thread a while ago. Other references for rp:

    G. Kreisel, Mathematical Logic , pp. 95-195 in Saaty (ed.) , Lectures on Modern Mathematics III , Wiley New York 1965.

    G. Kreisel and A. Lévy, Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems , Mathematical Logic Quarterly 14 (7-12):97–142, 1968.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2015
    • (edited May 1st 2015)

    Thomas,

    thanks a lot for all this!

    I have added these references with brief pointers to them to type of types and to reflection principle . Excellent.

    (and the bit related to mapping FOL into TT to Homotopy type theory FAQ – Why should I care? – For set theorists)

    • CommentRowNumber15.
    • CommentAuthorMichael_Bachtold
    • CommentTimeMay 2nd 2015
    • (edited May 2nd 2015)

    Re: #6: Thank you Todd. Unfortunately from your example el:1↓Set→Setel: 1 \downarrow Set \to Set I still don’t grasp how people think about the universal fibration Type^→Type\widehat{Type}\to Type, and why they call it “elements”.

    If I take a pointed set (x 0,X)(x_0,X), then

    el((x 0,X))=X,el((x_0,X))=X,

    which I read as “the elements of the pointed set (x 0,X)(x_0,X) are XX”. Notwithstanding that we are talking about terminology, which can’t be right or wrong, that doesn’t sound “right” :). Is there some other way to read it?

    I also wondered if el:1↓Set→Setel: 1 \downarrow Set \to Set is actually a universe in some (higher?) topos. Since the base of that fibration is SetSet my first guess was that this could be a universe in the topos of Sets, but I couldn’t make sense of that.

    Instead, naively thinking about a universe in the topos of sets, leads me to the following picture: a universe in the topos Set should be a set UU, such that global points of UU correspond to (small) sets in Set. Then U^\widehat{U} should be the disjoint union of all small sets ∑ ′X′∈UX\sum_{'X'\in U} X and the projection U^→U\widehat{U}\to U maps an element x∈Xx\in X to the name of the set XX that contains it. If this is right it seems more natural to call the arrow U^→U\widehat{U}\to U something like ContainerOfContainerOf or TypeOfTypeOf, in the sense that it maps a term to its type. Is that approximately right?

  16. Oh and thanks to Urs and the others for the clarifications concerning “reflects”. I need to think about that some more.

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 2nd 2015
    • (edited May 2nd 2015)

    The way I read it is that points in the fiber over XX correspond exactly to elements of XX, for every object X∈SetX \in Set.

    You might know this already, but this fibration el:Set *→Setel: Set_\ast \to Set is a universal fibration which classifies discrete fibrations, via the category of elements construction applied to a functor F:C→SetF: C \to Set. The category of elements el(F)el(F) is the (strict) pullback of el:Set *→Setel: Set_\ast \to Set along FF. In particular, even if we initially don’t like “elel” as notation for the universal discrete fibration Set *→SetSet_\ast \to Set, it is in fact the category of elements el(1 Set)el(1_{Set}) of the identity functor.

    More later.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2015
    • (edited May 2nd 2015)

    Michael,

    here some more replies:

    Along the lines of the discussion at object classifier in an (infinity,1)-topos, there are universal fibrations/bundles for all sort of kinds of objects/maps. The fibration that Todd mentioned, Set *→SetSet_\ast \to Set is the universal discrete Grothendieck fibration of discret categories. Strictly speaking, this happens in 2-topos theory. This is a good example for the general principle, but in itself maybe a little remote from the idea of universes here, which I think is what causes some of your puzzlement.

    The actual universe fibration that you are after

    Type^⟶Type \widehat Type \longrightarrow Type

    is simple to describe in words: its fiber over a name ′X′'X' down in the base is that very type XX of which ′X′'X' is the name.

    (I have added a comment to this extent to object classifier – Definition, scroll down a bit.)

    So if we give that map Type^→Type\widehat Type \to Type a name, say elel, and if we write, as usual el −1(−)el^{-1}(-) for the pre-image (fiber, homotopy fiber), then

    X≃el −1(′X′). X \simeq el^{-1}('X') \,.

    Now if one never writes down the universal type bundle Type^→Type\widehat Type \to Type itself but just needs this kind of formula for saying that a type is that given by a particular name, then one probably tends to not write the − −1{-}^{-1} here. Doing so is what leads to the notation that you see at type of types – Tarski style .

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMay 2nd 2015

    I don’t think it is appropriate to call the map Set *→SetSet_*\to Set “elel”. That should be name of the corresponding functor, sending each point to the fiber over that point, not the associated fibration.

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 2nd 2015

    The nLab uses the notation el(F)el(F) for the fibration associated to F:C→SetF: C \to Set, and I thought that was in fact pretty standard. I’ve never seen el(U)el(U) used to denote the functor C→SetC \to Set that classifies a discrete fibration U:E→CU: E \to C.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeMay 2nd 2015

    The nLab uses the notation el(F)el(F) for the fibration associated to F:C→SetF: C \to Set, and I thought that was in fact pretty standard.

    Yes, I think the standard thing is to use el(F)el(F) for the domain of that fibration. So el(Id Set)el(Id_{Set}) is another name for Set *Set_*, that’s fine. But I don’t think the functor Set *→SetSet_* \to Set should be called “elel”, as you wrote in #17.

    I wasn’t saying that el(U)el(U) should be the functor classifying a fibration UU. I was saying that “elel” (unadorned) is the “universal” type family, which categorically I guess you can think of as the identity functor of SetSet, or more precisely the inclusion of a small subuniverse of SetSet into it. So if X:UX:U is the “name” of a type, then el(X)el(X) is the corresponding type itself.

    • CommentRowNumber22.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 2nd 2015

    Mike, look at revision #1 of universe in a topos. You wrote el:E→Uel: E \to U!

    Since Urs called my name in another thread, I thought I’d give a shot at explaining my take on this notation in #6. But maybe you ought to be the one explaining things to Michael Bachtold, since it was evidently your notation.

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMay 3rd 2015

    Well, evidently I’ve learned something in the past 6 years. (-:

    • CommentRowNumber24.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 3rd 2015
    • (edited May 3rd 2015)

    Mike: please feel free to change it if you insist. Whatever anyone thinks of the appropriateness of the notation elel, it is at least explicable as notation for a universal category of elements fibration. That’s partly what Michael was asking about, and that’s what I was attempting to answer.

    I’m still not sure I’m following the point you’re making in #21 (sorry). This SetSet-valued functor you’re referring to (that you say is the thing we should mean by “elel”) is represented internally by a map E→UE \to U, where UU is the object part C 0C_0 of what I would call a universe object (which would be a certain internal category CC representing small sets and functions). I just don’t see what would be so wrong about calling that internal (co)presheaf E→UE \to U “elel”.

    • CommentRowNumber25.
    • CommentAuthorMichael_Bachtold
    • CommentTimeMay 3rd 2015
    • (edited May 3rd 2015)

    Re #17 & 18, that clears it up for me, thank you. I didn’t know of the universal property of Set *→SetSet_* \to Set so that also helped.

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeMay 3rd 2015
    • (edited May 3rd 2015)

    @Todd, what I think is wrong with it is what Michael said:

    If I take a pointed set (x 0,X)(x_0,X), then

    el((x 0,X))=X,el((x_0,X))=X,

    which I read as “the elements of the pointed set (x 0,X)(x_0,X) are XX”. Notwithstanding that we are talking about terminology, which can’t be right or wrong, that doesn’t sound “right”

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeMay 3rd 2015

    Oops, hit submit instead of preview. I was going to continue, I don’t object so much to calling the internal presheaf as a whole elel, but I don’t like calling the projection map from its total object to the universe elel. (The internal presheaf, of course, is a structure consisting of UU, EE, elel, and an action.)

    • CommentRowNumber28.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 3rd 2015

    Okay, thanks Mike. I guess we can agree on elel for the internal presheaf/functor then, although el:E→Uel: E \to U does strike me as a fairly innocuous abuse of language, since the action in this case is pretty canonical. Just so no one is offended, I’ll use π:E→U\pi: E \to U for the remainder of this comment.

    Continuing: universe in a topos doesn’t look too bad to me, but it might help to be a tiny bit more explicit. The full internal subcategory generated by π:E→U\pi: E \to U, discussed here, has as underlying graph ⟨d 0,d 1⟩:U 1→U×U\langle d_0, d_1 \rangle: U_1 \to U \times U the exponential (1×π) π×1(1 \times \pi)^{\pi \times 1} of the two objects 1×π:U×E→U×U1 \times \pi: U \times E \to U \times U and π×1:E×U→U×U\pi \times 1: E \times U \to U \times U in the slice topos Set/U×USet/U \times U. Over a point (x,y):1→U×U(x, y): 1 \to U \times U, the fiber of the exponential is isomorphic to π −1(y) π −1(x)\pi^{-1}(y)^{\pi^{-1}(x)} in SetSet, i.e., the full set of functions between the sets or types π −1(x)\pi^{-1}(x), π −1(y)\pi^{-1}(y) named by x,yx, y.

    I’m feeling a little lazy right now, so I won’t write out the rest of the internal category structure.

    The action α:E× UU 1→E\alpha: E \times_U U_1 \to E, where the domain is the fiber product of π:E→U\pi: E \to U and d 0:U 1→Ud_0: U_1 \to U (but fibered over UU with the help of d 1:U 1→Ud_1: U_1 \to U), is the expected one, which over a point y:1→Uy: 1 \to U looks like a bundled collection of evaluation maps

    ∑ x∈Uπ −1(y) π −1(x)×π −1(x)→π −1(y).\sum_{x \in U} \pi^{-1}(y)^{\pi^{-1}(x)} \times \pi^{-1}(x) \to \pi^{-1}(y).

    We could go on and use the axioms of the article to see this internal functor elel as providing a subtopos embedding into SetSet (in the sense of the subsection on indexed categories). That’s more or less how I would understand a universe object in this context: as an internal topos object, forming a full subtopos on passage to indexed categories.

    • CommentRowNumber29.
    • CommentAuthorThomas Holder
    • CommentTimeMay 4th 2015
    • (edited May 5th 2015)

    I have added a reference at universe in a topos to an earlier note of Hofmann and Streicher (pdf) that contains a very explicit discussion of the presheaf case and might be helpful for clarifying concept&notation.

    As Streicher (2005) points out that the existence of a universe with NNO in the free topos with NNO would amount to an internal consistency proof of arithmetic I wonder if it would be licit to think of the existence of a universe as a kind of ’consistency’ in other cases.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeMay 5th 2015

    el:E→Uel: E \to U does strike me as a fairly innocuous abuse of language

    Thinking about this some more, I think in general I tend to eschew synecdoche as applied to the names of morphisms. This applies even in the degenerate case of, say, objects in a slice category C/AC/A, where I would tend to refer to p:B→Ap:B\to A as “BB” and regard it as implicitly equipped with the structure of pp, rather than referring to it (less ambiguously!) as “pp”. Probably this is partly due to type discipline; it doesn’t make sense to me to talk about “pp” without having previously specified both its domain and codomain. We could similarly refer to a group (G,m:G×G→G,e)(G,m:G\times G\to G,e) as just “mm”, but we don’t. Also I think I feel more strongly that the name of a function should indicate what that function does to its inputs, rather than anything more general or abstract about how that function was constructed or what it represents.

    • CommentRowNumber31.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 5th 2015

    Also I think I feel more strongly that the name of a function should indicate what that function does to its inputs, rather than anything more general or abstract about how that function was constructed or what it represents.

    That is quite understandable (and surely what was confusing about the notation in the first place). I thought of el^:E→U\widehat{el}: E \to U or el˜:E→U\tilde{el}: E \to U as possible substitutes, to indicate these are constructs derived from another concept “elel”.

    Although now that I think of it, I don’t recall whether people generally denote internal presheaves by a notation other than (say) (F:X→C 0,α:C 1× C 0X→X)(F: X \to C_0, \alpha: C_1 \times_{C_0} X \to X) but which they are secretly thinking of as a functor F:C op→SetF: C^{op} \to Set or F:C op→EF: C^{op} \to \mathbf{E}. Do they?

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeMay 5th 2015

    I like el^\hat{el} or el˜\tilde{el}. I don’t know the answer to your question.

1 to 32 of 32

  1.