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.
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.
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?
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.)
I find myself having a lot less time for editing the nLab these days than I used to, for some reason…
Some follow-up questions: in universe in a topos, the universal arrow is denoted with . What does abbreviate?
A similar notation 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 .
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 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).
The would stand for elements. You can think of this as akin to the fibration which projects a pointed set down to its underlying set.
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.
I have looked up a few more authors that speak about type universes as “reflections” of the ambient type system, here.
Introducing universes can be considered as a reflection principle: such a universe reflects those types whose names are its objects.
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.
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
I gave reflection principle a stub. Is it sensible to list it in the list at foundational axiom?
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.
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)
Re: #6: Thank you Todd. Unfortunately from your example I still don’t grasp how people think about the universal fibration , and why they call it “elements”.
If I take a pointed set , then
which I read as “the elements of the pointed set are ”. 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 is actually a universe in some (higher?) topos. Since the base of that fibration is 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 , such that global points of correspond to (small) sets in Set. Then should be the disjoint union of all small sets and the projection maps an element to the name of the set that contains it. If this is right it seems more natural to call the arrow something like or , in the sense that it maps a term to its type. Is that approximately right?
Oh and thanks to Urs and the others for the clarifications concerning “reflects”. I need to think about that some more.
The way I read it is that points in the fiber over correspond exactly to elements of , for every object .
You might know this already, but this fibration is a universal fibration which classifies discrete fibrations, via the category of elements construction applied to a functor . The category of elements is the (strict) pullback of along . In particular, even if we initially don’t like “” as notation for the universal discrete fibration , it is in fact the category of elements of the identity functor.
More later.
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, 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
is simple to describe in words: its fiber over a name down in the base is that very type of which 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 a name, say , and if we write, as usual for the pre-image (fiber, homotopy fiber), then
Now if one never writes down the universal type bundle 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 here. Doing so is what leads to the notation that you see at type of types – Tarski style .
I don’t think it is appropriate to call the map “”. That should be name of the corresponding functor, sending each point to the fiber over that point, not the associated fibration.
The nLab uses the notation for the fibration associated to , and I thought that was in fact pretty standard. I’ve never seen used to denote the functor that classifies a discrete fibration .
The nLab uses the notation for the fibration associated to , and I thought that was in fact pretty standard.
Yes, I think the standard thing is to use for the domain of that fibration. So is another name for , that’s fine. But I don’t think the functor should be called “”, as you wrote in #17.
I wasn’t saying that should be the functor classifying a fibration . I was saying that “” (unadorned) is the “universal” type family, which categorically I guess you can think of as the identity functor of , or more precisely the inclusion of a small subuniverse of into it. So if is the “name” of a type, then is the corresponding type itself.
Mike, look at revision #1 of universe in a topos. You wrote !
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.
Well, evidently I’ve learned something in the past 6 years. (-:
Mike: please feel free to change it if you insist. Whatever anyone thinks of the appropriateness of the notation , 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 -valued functor you’re referring to (that you say is the thing we should mean by “”) is represented internally by a map , where is the object part of what I would call a universe object (which would be a certain internal category representing small sets and functions). I just don’t see what would be so wrong about calling that internal (co)presheaf “”.
Re #17 & 18, that clears it up for me, thank you. I didn’t know of the universal property of so that also helped.
@Todd, what I think is wrong with it is what Michael said:
If I take a pointed set , then
which I read as “the elements of the pointed set are ”. Notwithstanding that we are talking about terminology, which can’t be right or wrong, that doesn’t sound “right”
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 , but I don’t like calling the projection map from its total object to the universe . (The internal presheaf, of course, is a structure consisting of , , , and an action.)
Okay, thanks Mike. I guess we can agree on for the internal presheaf/functor then, although 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 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 , discussed here, has as underlying graph the exponential of the two objects and in the slice topos . Over a point , the fiber of the exponential is isomorphic to in , i.e., the full set of functions between the sets or types , named by .
I’m feeling a little lazy right now, so I won’t write out the rest of the internal category structure.
The action , where the domain is the fiber product of and (but fibered over with the help of ), is the expected one, which over a point looks like a bundled collection of evaluation maps
We could go on and use the axioms of the article to see this internal functor as providing a subtopos embedding into (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.
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¬ation.
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.
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 , where I would tend to refer to as “” and regard it as implicitly equipped with the structure of , rather than referring to it (less ambiguously!) as “”. Probably this is partly due to type discipline; it doesn’t make sense to me to talk about “” without having previously specified both its domain and codomain. We could similarly refer to a group as just “”, 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.
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 or as possible substitutes, to indicate these are constructs derived from another concept “”.
Although now that I think of it, I don’t recall whether people generally denote internal presheaves by a notation other than (say) but which they are secretly thinking of as a functor or . Do they?
I like or . I don’t know the answer to your question.
1 to 32 of 32