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.
Has the infinity version of a logical morphism been developed? I couldn’t find it in Lurie.
Wouldn’t that presuppose a notion of higher elementary topos?
It’s an interesting question to think about, though. Obviously a logical functor should preserve finite limits and colimits and dependent exponentials, and if we include any HIT-like things in our definition of higher elementary topos then a logical functor should preserve those too. But in what sense should it “preserve universes”, given that object classifiers are not unique?
Would it not be good enough to send object classifiers to object classifiers? Or is there somewhere in type theory where it really matters that one universe is the immediate successor of another?
What exactly does “send object classifiers to object classifiers” mean?
In this context, I suppose “object classifier” would have to mean whatever is needed to interpret type-theoretic universes – a classifying object, a universal bundle, closed under certain operations, etc.
That’s reasonable. But then it seems a little odd that a “logical functor” between -toposes doesn’t induce a logical functor between their underlying 1-toposes.
That’s an interesting point. I want to say that’s because the subobject classifier in a 1-topos corresponds to an impredicative , which is somehow an extra structure that needs to be preserved separately. Equally, it suggests a notion of “lax” logical morphism between 1-toposes that preserves everything except possibly the subobject classifier.
Equivalently, one could go the middle road, and just ask that the comparison morphism has certain properties, for instance is -truncated.
a notion of “lax” logical morphism between 1-toposes that preserves everything except possibly the subobject classifier
Would that be just a finitely-cocontinuous locally cartesian closed functor?
just ask that the comparison morphism has certain properties, for instance is (−1)-truncated.
In the 1-topos case I think the Elephant discusses “sub-logical” functors. In the -case, there is no “the” comparison map since object classifiers are not unique, but I guess since each object classifier embeds in the next one it doesn’t matter for this condition.
Would that be just a finitely-cocontinuous locally cartesian closed functor?
Plus whatever inductive types we want to make use of, I guess. There’s a result (B2.5.6 in the Elephant), apparently due to Freyd, that says that any functor between toposes preserving finite colimits must also preserve NNOs, so some inductive types do not need to be explicitly preserved.
Also, isn’t there some suggestion that universes are a kind of inductive-recursive type?
isn’t there some suggestion that universes are a kind of inductive-recursive type?
I don’t think so, not really in the sense that’s relevant here.
I’m not sure exactly what Zhen Lin had in mind, but it certainly seems possible to me to define a ’type of universes’ if one has mutually recursive types, which I think are the same as the ’inductive-recursive’ types that Zhen Lin mentioned. The mutuality is crucial here: one defines the universes and the rules for each universe inductively, and each relies upon the other. That is to say, writing out this construction for the first few steps: begin with (thought of as the empty universe); we then introduce , add , and add the rules for which we can use to build types (so everything will be built up from , which will not give very many possibilities!); we then introduce and its rules, which we can use to build up types from and ; etc.
A long time ago, I actually tried to implement this in Agda! (Agda has mutually recursive types, or one flavour of them at least). At that time, there was only really Voevodsky’s short early sketch on the homotopy -calculus that, as far as I knew, was circulating, and in that document this point of view, of ’building everything up from nothing’, is emphasised. It does not seem to have attracted much attention in the ensuing development of HoTT, but I am still fond of that picture.
All this is of course closely related to the question of ’defining Martin-Löf type theory within Martin-Löf type theory’.
I seem to recall that there was a paper not too long ago which discussed defining a mutually recursive type of universes in the manner I sketched, but I cannot find it just now.
I do not know if mutually recursive types would have a good interpretation in an -topos as we know the notion today, though.
Zhen, Mike and Richard, Thanks for the nice input. Indeed, we are trying to do something in type theory and would like to see what has been done in higher topos theory. I am glad I have not overlooked something obvious.
There is elementary+(infinity,1)-topos of course.
Of course, inductive-recursive universes are well-known in type theory, and with higher induction-recursion you can get univalent ones as well. What I meant to say is that not every universe is inductive-recursive, so preserving universes is not a special case of preserving inductive(-recursive) types.
Thanks for the clarification!
It seems to me that a type of universes defined as a mutually recursive type (in one flavour or another) captures rather precisely what a universe should be. There may of course be some restrictions in the rules that one can define, coming from the precise details of how one defines a mutually inductive type. But in principal, it seems to me that one should be able to figure out a definition of the latter which allows one to capture any reasonable situation, as has presumably been done for ’higher mutually recursive types’.
Thus I think that it might be perfectly reasonable to think of an ’elementary -topos’ as having something corresponding to a ’universe type’, and asking that a logical functor preserve such a thing. But I have no idea how to think of mutually recursive types in this semantics. Indeed, the semantics of mutually recursive types seems to me to be a rather interesting topic, because they are rather powerful: a single one allows one to build the whole of mathematics! (Of course this statement is an over-simplification, but I think there is some truth to it, that is interesting to contemplate.)
To try to clarify a little further: although there could be all kinds of universes, depending on which rules we allow, an elementary -topos (however it turns out to actually be defined) need not have universes of all of these kinds. It seems to me that one could decide upon whatever kind(s) of universe one wishes to work with, and then one could have a corresponding notion of elementary -topos, in which one asks for a mutually recursive type of the right kind(s) (just like one might ask for a natural numbers object), and asks that logical functors preserve it/them. There could be ’weaker’ notions of logical functor which take universes ’of any kind’ to universes ’of any kind’.
I think there is room for different conceptions of what a universe “should” be. There’s quite a good argument that the defining feature of a universe is that it’s closed under certain operations, which is a very different thing from being inductively generated by those operations. For instance, larger large cardinals seem impossible to reach with currently-known sorts of inductive definition (induction-recursion is derivable from an axiom that says roughly “the cardinality of the class of all sets is Mahlo”), but still ought to count as universes.
There’s the additional problem that in order to define an inductive-recursive universe, you usually have to already have a universe for the types it contains to live in. And if we have a functor that doesn’t preserve that “ambient” universe, I’m not sure whether it makes sense to even ask whether it preserves the inductive-recursive universe.
(Note that induction-recursion is different from what are usually called “mutual inductive types” – the latter are essentially just inductive families indexed by a finite set.)
I agree, however, that there seems to be room for many variations in the notion of -logical functor.
Regarding your first paragraph: yes, indeed, I am referring only to the ’inductively generated’ notion of universe, as you put it. That is to say, I am thinking a universe as being (some flavour of) Martin-Löf type theory, but where there is a special type (the universe at the next level below) whose terms can be viewed as types. If one defines a universe differently, then of course I agree that this opens up further possibilities. I find the question of ’what happens next’ for universes after the usual hierarchy to be very interesting, but I think that we are a very long way away from having mathematics that lives fundamentally at this level (I do not know of any interesting, naturally occurring mathematics which is ’large enough’ to fundamentally need more than ’very large’ categories; I am not regarding large cardinal set-theoretic stuff as ’natural’ here, which is not of course to say that it is not interesting in its own right). This is no doubt related to the fact that current forms of inductive types cannot capture this ’leap’ naturally.
Regarding your second paragraph: I do not see the problem here. The elementary -topos itself would, it seems to me, be playing the role of the ’ambient universe’ here. But it is not really possible for us to discuss this point properly, because so many things are unclear (such as the semantics of mutually recursive types, and whether an elementary -topos can be thought of as having them).
Regarding your third paragraph: I understand the difference, but would like to have a terminology which emphasises the mutuality, which is what is really significant. But the terminology ’mutually recursive’ maybe indeed introduces its own possibilities for confusion!
You need at least a sort of “large elimination” for inductive-recursive types in order to define a universe that way, but you could assume that explicitly as a categorical property of such types instead of having a universe object given.
I think the terminology “inductive-recursive” is already supposed to emphasize that the induction and the recursion are happening mutually. “Mutually recursive” generally refers only to groups of functions defined by recursion (perhaps over a mutually inductive family of types).
Yes, that is the sort of thing that I had in mind.
You are probably correct that I should avoid the terminology ’mutually recursive’. I’m not very keen on ’inductive-recursive’ either, but I should use a term that does not create a different kind of confusion!
1 to 21 of 21