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.
I decided it would be a good idea to split off realizability topos into a separate entry (it had been tucked away under partial combinatory algebra). I’ve only just begun, mainly to get down the connection with COSHEP. A good (free, online) reference is Menni’s thesis.
Added a pointer to
and added the statement of the theorem it proves, here.
Thanks; I still need to read that article. The global sections is not a geometric morphism for a realizability topos, though, is it? I mean, it is in the other direction, but in the statement wouldn’t it be more correct to say “the global sections functor has a right adjoint”?
I’m surprised that he doesn’t need to assume extensivity.
True, I have fixed it now.
Urs, I see that you wrote “closed” instead of “prone” – actually I like that since it generalizes “closed mono” in the context of localizations/universal closure operations/cartesian reflectors or whatever you want to call them. Are there other authors who use “closed” in this generalized sense?
I corrected two minor mistakes in the article – a mixture of nabla and Delta, and discrete objects are only right orthogonal to closed regular epis, not arbitrary closed maps.
Concerning the confusion of nabla and Delta: this confusion has a long history. The situation is that Gamma has a right adjoint for realizability toposes that one wants to call nabla in analogy to the situation in Grothendieck toposes. But this right adjoint is the “constant objects functor” which exists for every tripos-induced topos, and for “localic” triposes the constant objects functor is actually left adjoint to Gamma. For now I put nabla everywhere, but if you prefer Delta I’m fine with that as well.
Jonas,
ah, thanks for fixing those glitches. Sorry.
Regarding “closed”: for idempotent monads at least I picked this up from
and then it played a central role in the discussion of modal homotopy types and cohesion, notably in Mike’s formalization.
I like it better than “prone” because it seems to be a much more general concept. On the other hand, it is a bit of abuse of terminology if the monad is not idempotent.
But the real reason I put it into the entry was that it allowed me to quickly link to an existing definition without having to type it afresh. If you have time and energy, you should please feel invited to edit the entry further and feel free to change whatever I jotted down there.
I like closed as well, and anyway nabla.Gamma is an idempotent monad so it fits exactly. I might make a revision of the article where I change it. Actually I wrote uniform instead of prone in earlier versions since there is a relation with “uniform objects” in realizability toposes, but then I realized that uniform should be more general (I think it should be defined as left orthogonal to discrete) which is why I changed it. Concerning the paper you cited, I realized that it’s relevant but I didn’t read it entirely since it’s quite long.
I’m not very familiar with your work on modal homotopy types, but from what I gathered it seems to be related to chains of adjunctions, and similar ideas are relevant in realizability as well.
Oh, of course, since the global sections are literally maps out of the terminal object here.
I have edited the axioms to make that come out more transparently, please check again here.
I added “finite-limit preserving” to “idempotent monad” since I think that’s an important property of and the setting where concepts like separated, closed, and dense behave well.
I wonder if there is a preferred terminology for “finite-limit preserving idempotent monad” on the nlab. I know that Johnstone calls them cartesian reflector, and that they are called localizations e.g.\ in the paper that Urs mentioned earlier.
I added “finite-limit preserving” to “idempotent monad” since I think that’s an important property of and the setting where concepts like separated, closed, and dense behave well.
Definitely.
I wonder if there is a preferred terminology for “finite-limit preserving idempotent monad” on the nlab. I know that Johnstone calls them cartesian reflector, and that they are called localizations e.g.\ in the paper that Urs mentioned earlier.
I usually just call them lex idempotent monads. I would have thought that “reflector” would refer to a left adjoint part, and I think I’d say the same for “localization”.
I have a question about the article: on a quick skim I wasn’t able to puzzle out exactly where local cartesian closure is needed.
I have a question about the nLab article realizability topos: why is all that space at the bottom? It seems to have been put there for a reason.
I put vertical whitespace at the bottom of entries whenever I am linking to references-items in the entry from elsewhere. Because if there is not a screen worth of entry below any anchor point, then linking to it is practically impossible, since the user will see not the intended target, but whatever is one screen height above the bottom.
Okay, thanks, I think I understand. It’s the first time I’ve ever noticed it (maybe because most articles have more than one bibliographic entry, and I guess you’d rather not apply that trick in case there are several references).
Mike: locally cartesian closure is necessary to reconstruct the application from the computable functions. The idea is that the application in the PCA is the realizer of evaluation in the (w)(l)ccc sense. Technically, application is reconstructed via ‘functional completeness’ of DCOs, see Theorem 5.11.
Thanks!
One thing I find interesting is that your hypotheses automatically imply that the category is extensive (since it is a topos), even though that isn’t explicitly assumed. I don’t suppose there is a more direct proof that those hypotheses imply extensivity, without going through the proof that it is a realizability topos?
I’m also intrigued by the analogy between your object and the “bound” of a bounded geometric morphism. I don’t suppose you have any more to say about that?
Mike, you rase two central issues here on which I have a whole lot to say, but I don’t know exactly how to start. So I just do it in no particular order.
On extensivity: there is an analogue with prehsheaf toposes. Presheaf toposes are extensive since colimits are “freely added”. Realizability toposes are generalized presheaf toposes in a sense, so it makes sense that they are extensive. However, one has to be careful here. The way realizability toposes can be understood as generalized presehaf toposes is via fibrations – concretely the gluing fibration of along the constant objects functor is the cocompletion of the family fibration of from finite-limit prestacks to fibered pretoposes (in the sense of my thesis). The analogy to presheaf toposes is that if is a meet-semilattice, then the gluing fibration of the presheaf topos of along is the same kind of cocompletion of the family fibration of . The subtlety is that the fibrational cocompletion only adds coproducts in the sense of left adjoints to change of fiber, and these do only coincide with ordinary colimits in the glued category if the gluing fibration coincides with the family fibration, which is precisely when the constant objects functor has a right adjoint. So the “fibered pretopos completion” might result in a fibration whose fibers don’t have any colimits. In fact, fibered pretoposes are precisely the gluing fibrations of functors with exact , so “fibrational extensivity” comes totally for free – see also Moens’ theorem in “Fibred categories a la Benabou” by Streicher.
This doesn’t answer your question, since I think you are interested in finite colimits in the glued category.
One way I understand this is via second order logic: In second order logic, disjunction and existential quantification can be defined in terms of the other connectives by universally quantifying over , and this is very related to the fact that we get coproducts for free in elementary toposes. Extensivity is then a manifestation of commutation laws of intuitionistic logic.
In this connection it is interesting to look at related construction that are predicative, and where one can’t perform the second order constructions. A precise instance of this is given by realizability over typed pcas. I think realizability categories over typed pcas do not generally have coproducts, but I don’t have a counterexample.
On : yes, that’s the bound. It is helpful to compare to presheaves on meet-semilattices in the presentation sketched above. In general, a bound for presehaf toposes is given by the coproduct of all representables. In our case, the mono can be viewed as the internal family of all representables in the gluing fibration along , and is its internal coproduct.
In all the above it becomes apparent that should be called in a fibrational context, since it takes the role of functor along which we glue. If we call the constant objects functor , then , being its left adjoint, deseves to be called , and we can view the situation as generalization of ‘totally connected geometric morphisms’. From this point of view, can be viewed as decomposition of into connected components.
Thanks! I should go read your thesis. I recall now that we had a bit of discussion back here. Can you complete the analogy “presheaf topos : realizability topos :: sheaf topos : ?”
On the completion of the scheme
presheaf topos : realizability topos
sheaf topos : ?
My basic point of view is that tripos-induced toposes are a generalization of localic toposes. in the following I will focus on this generalized localic case (although the question of finding a common framework for realizability and non-localic grothendieck toposes is interesting as well). Thus I modify your question to
localic presheaf topos : realizability topos
localic topos : ?
The best candidate for (?) I have is “tripos-induced topos such that ”. I call this condition “realizability-like” at one point in my thesis.
I can show that whenever is a tripos-induced topos, then there exists a realizability-like such that is localic over i.e. there exists a localic geometric morphism from to . This can be viewed as a decomposition result for constant objects functors, opposite to “Pitts iteration” (the result that constant objects functors coming from triposes on different bases comopose). However, there are some problems with this result. Firstly, the composition is not unique even to equivalence, and secondly I have the feeling that in order to have a well behaved theory of triposes on arbitrary bases (generalizing the theory of localic geometric morphisms), one should consider “enriched triposes” or “fibered triposes”. This reminds me that I wanted to look into your enriched indexed categories. I hope I find time for that soon.
Are there examples of tripos-induced toposes that are neither localic nor realizability?
Enriched indexed categories are on the reading list of the Kan extension seminar, so there will be a cafe post about them sometime soonish.
Could there be a homotopified version - a realizability -topos?
Mike: if you mean the restrictive definition of “realizability-like” by then even most realizability constructions are not “realizability-like”: relative realizability, modified realizability, Krivine realizability and the Dialectica construction don’t fulfill this criterion I think. So maybe “realizability-like” is not such a good name for the concept. On the other hand, extensional realizability is “realizability-like”, but not “presheaf-like”. The definitions of relative, modified, and extensional realizability triposes and toposes can be found in Jaap van Oosten’s book “Realizability: an introduction to its categorical side”.
David: good question, I don’t know enough about -toposes. I don’t really see how to how to add higher dimensional aspects to the logical/operational intuition about realizability, but maybe one could try to give an -analogue of the characterization of realizability toposes? A thought on the syntactic approach: in homotopy type theory, the link between higher categories and syntax is given by identity types. Realizability, however is intrinsically untyped, so it is not obvious how to make the connection. But there are lambda-terms that behave like symmetries, e.g. by permuting a list of arguments. Maybe one could use them as invertible 2-cells in an appropriate context?
Regarding the -version: I would just look for the obvious (if any) homotopy-theoretic analogs of your axioms and let the result answer the question of what -realizability is.
For some of the axioms this is obvious:
lcc goes to locally cartesian closed (infinity,1)-category;
exactness goes to groupoid objects in an (infinity,1)-category are effective;
the faithful adjoint goes to a faithful adjoint (infinity,1)-functor.
I am not sure what to do about the projective objects though.
There are two approaches:
Consider the cubical set model in the effective topos. This should be an elementary higher topos in the sense of Joyal.
van Oosten’s model structure on the effective topos
@Jonas: Hmm, in that case I find the characterization theorem somewhat less interesting. I would have hoped for a characterization theorem that includes everything that people call “realizability”.
I think the right construction of a realizability -topos would be to define -exact completion and then apply that in place of the 1-exact completion. Awodey-Bauer have worked on something similar in the (2,1)-case. Cubical/simplicial sets in a realizability topos would be taking the 1-exact completion and then after that the -exact completion, which probably isn’t right since exact completion (in the sense of ex/lex completion) isn’t idempotent.
Van Oosten’s model structure is intriguing, but my impression is that it’s seeing something different, more akin to the “geometric” homotopy theory in a cohesive topos.
Sorry to disappoint you, Mike. To give you all the bad news at once, let me also tell you that the characterization result in the form given in the article depends on the axiom of choice. I write that at the end of the introduction. Realizability toposes over PCAs are only exact completions in the presence of choice, since this is needed to show that partitioned assemblies are projective. Without choice, you have to replace the usual projectivity by a kind of “fibrational projecitivity”, relative to the gluing fibration along the constant objects functor. This is done in my thesis.
Concerning a characterization of “everything that people call realizability” – the problem is that the field is simply not very clearly delimited, and I cannot imagine logicians to reach a consensus on the “essence” of realizability very soon. First of all we have to give up toposes since typed realizability interpretations give predicative models. In relatively recent work, the logician Jean-Luis Krivine argues that realizability should be a generalization of forcing, and introduces a notion of “realizability algebra” that comprises all complete boolean algebras. Krivine is only interested in classical logic, but if we drop this restriction then following his philosophy it would be reasonable to include all locales and localic toposes. At this point, a natural candidate for a general notion of realizability is “all triposes” in my opinion.
In his 1982 thesis, Andy Pitts gave a characterization of all tripos-induced toposes together with their constant objects functors . The explicit inclusion of the constant objects functor in the characterization seems necessary, and a way to understand this is to observe that the constant objects functor is equivalent to a fibering of the topos over via Moens’ theorem. One might say that “realizability toposes are fibered toposes”. The fact that we can avoid mentioning the constant objects functor explicitly in the characterization of realizability over PCAs is kind of a coincidence – it is since it is adjoint to the global sections functor in this case.
Summarizing could take the point of view that your question for a characterization of “all of realizability” has already been answered by Pitts (at least in the impredicative case). More on this in Section 1.2 of my thesis.
[And a remark on the homotopy issue: van Oosten talks about a notion of homotopy in realizability toposes (over PCAs), but I think he doesn’t claim it is an actual model structure.]
@Mike, could you recall for me the statement about exact completion that you have in mind?
So I understand that is the exact completion of (partioned assemblies). But for using this for an -categorical generalization we would then need to know the -version of . Is it clear what that should be?
I know almost nothing about realizability, so I may well be missing something really basic here. But I observe that to the extent that Jonas’s axioms really are analogous to Giraud’s axioms, as he suggests they are, then since the -version of Giraud’s axioms does give Grothendieck -toposes, it would seem really natural to ask for the -version of Jonas’s axioms. (“Frey’s axioms”, I should say, for Google :-)
Actually I have a more general question (and maybe too general a question): given that we now have an axiomatic formulation of what was previously defined only very explicitly in components, does looking at the axioms make anyone of you want to streamline them further and then declare the result to be a new, more general definition of realizability? One that is justified not (just) by concrete constructions, but by abstract properties?
I’m not saying it’s not natural to look for the -analogue of Jonas’ axioms, but we should also look for the construction that such axioms would characterize. And the fact that the axioms don’t capture “the whole theory of realizability” suggests to me that it’s more important to focus on the constructions.
As for an -version of , exact completion is analogous to the category of sheaves on a site (in a very precise sense), and when we pass to -sheaves we don’t always need to make the 1-site into an -site; it often suffices to consider -sheaves on the same 1-site. So while it’s also natural to wonder about an -version of , I don’t think it’s necessary.
Maybe after the semester is over I’ll have time to read your thesis. In the absence of AC, can you consider a RT to be one of my generalized exact completions relative to a unary site, e.g. with covers induced by the surjections of sets?
The appearance of fibrations is not all that surprising to me, e.g. the version of Giraud’s theorem for a general base topos also requires a fibered category as input. There also ought to be a version of generalized exact completion for a fibered category, e.g. arity classes are naturally described as families of morphisms in the base category. I seem to remember speculating about this at some point on the cafe, but I didn’t see it in the obvious post that I linked to above. Maybe it was somewhere else.
Reading Mike’s and Urs’ comments (25, 27), I realize that I should have been more careful when writing the abstract. I brought up Giraud’s theorem since Johnstone pointed out the lack of such a result for realizability when comparing Grothendieck toposes to realizability toposes. As a first approximation the comparison is ok, simply in the sense that they give characterizations of classes of categories that were previously only described by constructions. However, on closer inspection there are differences – most imporantly, realizability toposes shouldn’t be viewed in analogy to sheaf toposes, but to localic presheaf toposes on meet-semilattices. In particular, the central role of projective objects is in analogy to Martha Bunge’s characterization of presheaf toposes as toposes having a generating family of indecomposable projectives (“Internal presheaf toposes”, 1973). I’ll try to make this more clear in a future revision.
My result characterizes a very particular class of toposes, and I agree with Mike that one should study more general classes. In my post from yesterday I suggested the class of all “tripos-induced toposes”, and I really think that this is a good framework. As I said, a “Giraud style characterization” of fibered tripos-induced toposes was in a sense already given by Pitts in his thesis – his characterization of constant objects functor can be translated into such a characterization via Moens’ theorem. Let me spell this out explicitely.
Pitts’ characterization of constant objects functors: A finite-limit preserving functor into a topos is a constant objects functor into a tripos-induced topos, iff
This translates into the following characterization of indexed/fibered toposes via Moens’ theorem:
An indexed category is (the indexed category corresponding to) the gluing fibration of a tripos-induced topos along the constant objects functor, iff
[All this works only with choice, without choice we need some regularity and pre-stack conditions]
It is illuminating to compare the characterization of constant objects functors to the characterization of localic geometric moprhisms. A localic geometric morphism into can simply be characterized as a finite limit preserving functor into a topos which has a right adjoint. Now the existence of the right adjoint is equivalent to local smallness of the gluing fibration in a fibrational sense (see Streicher’s notes). Thus, tripos induced toposes are generally not locally small fibrationally. This explains why we need condition 4 explicitly above – if the fibration was locally small, then it would also be well powered and the existence of a generic family of subterminals would come for free.
@Mike in 30: Yes, you can use unary topologies in absence of choice, as Wouter Stekelenburg pointed out here. In this case the unary covers are the epicartesian maps, i.e. cartesian arrows over surjective functions in the fibration .
What a great thread this is. I had been thinking about one of the topics here, namely the possibility of higher effective/realizability toposes, and whether directly adjoining higher inductive types to the semantics of an effective topos would successfully promote it to a higher setting. This is desirable if we want to discuss, for example, notions of computability adapted to homotopy type theory.
There’s now the work on cubical assemblies and on [path categories]. There’s some more discussion on the HoTT nlab here, but that page needs updating.
This seems to be described also at partial combinatory algebra.
Re #36: yes, and also at tripos. I just didn’t like the look of the one subsection just saying “see tripos”; it didn’t seem very friendly to the reader. The natural place to put the construction would be on a page like realizability tripos, but it seems natural to include at least the basic definition within the text of all three pages. I suppose we could eliminate the redundancy by making it a snippet that gets !included into all three pages, but I’m not sure that’s worth the effort.
Nah, it wasn’t criticism of what you did; I just didn’t know whether you’d seen it. It’s all fine.
1 to 40 of 40