The extent function for an assembly must take values in *nonempty* subsets.

Nah, it wasn’t criticism of what you did; I just didn’t know whether you’d seen it. It’s all fine.

]]>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 `!include`

d into all three pages, but I’m not sure that’s worth the effort.

Added the fact that a realizability topos is also an ex/reg completion of the non-partitioned assemblies, and that the ex/lex completion property depends on choice in Set.

]]>This seems to be described also at partial combinatory algebra.

]]>Added a sketch of the construction of the realizability tripos over a PCA.

]]>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.

]]>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.

]]>@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 $\mathbf{PAsm}\to\mathbf{Set}$.

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 $\Delta:\mathrm{Set}\to\mathcal{E}$ into a topos is a constant objects functor into a tripos-induced topos, iff

- $\Delta$ is bounded by $1$ ( every $A$ in $\mathcal{E}$ is a subquotient of some $\Delta I$)
- the indexed poset $\mathrm{sub}_{\mathcal{E}}\circ\Delta$ has a generic predicate ($\mathrm{sub}_{\mathcal{E}}$ is the subobject fibration of $\mathcal{E}$)

This translates into the following characterization of indexed/fibered toposes via Moens’ theorem:

An indexed category $\mathcal{E}:\mathbf{Set}^{\mathrm{op}}\to\mathbf{Cat}$ is (the indexed category corresponding to) the gluing fibration of a tripos-induced topos along the constant objects functor, iff

- All fibers are toposes
- $\mathcal{E}$ has
*internal sums*, i.e. all change of fiber maps $f^*:\mathcal{E}(I)\to\mathcal{E}(J)$ have left adjoints $\Sigma_f$ subject to the Beck-Chevalley condition - Every $X\in\mathcal{E}(1)$ is a subquotient of some $\Sigma_I 1$
- There exists a
*generic family of subterminals*, i.e. a mono $m:U\to 1$ in some $\mathcal{E}(A)$ such that every subterminal in any of the fibers of $\mathcal{E}$ can be obtained as reindexing of $m$.

[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 $\mathbf{Set}$ can simply be characterized as a finite limit preserving functor $\Delta:\mathbf{Set}\to\mathcal{E}$ 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.

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.

]]>I’m not saying it’s not natural to look for the $\infty$-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 $\infty$-version of $PAss(A)$, exact completion is analogous to the category of sheaves on a site (in a very precise sense), and when we pass to $\infty$-sheaves we don’t always need to make the 1-site into an $\infty$-site; it often suffices to consider $\infty$-sheaves on the same 1-site. So while it’s also natural to wonder about an $\infty$-version of $PAss(A)$, I don’t think it’s necessary.

]]>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?

]]>@Mike, could you recall for me the statement about exact completion that you have in mind?

So I understand that $RT(A)$ is the exact completion of $PAss(A)$ (partioned assemblies). But for using this for an $\infty$-categorical generalization we would then need to know the $\infty$-version of $PAss(A)$. 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 $\infty$-version of Giraud’s axioms does give Grothendieck $\infty$-toposes, it would seem really natural to ask for the $\infty$-version of Jonas’s axioms. (“Frey’s axioms”, I should say, for Google :-)

]]>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 $\mathcal{E}$ together with their constant objects functors $\Delta:\mathrm{Set}\to\mathcal{E}$. 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 $\mathrm{Set}$ 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.]

]]>@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 $(\infty,1)$-topos would be to define $\infty$-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 $\infty$-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.

]]>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

Regarding the $\infty$-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 $\infty$-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.

]]>Mike: if you mean the restrictive definition of “realizability-like” by $\Gamma\dashv\Delta$ 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 $\infty$-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 $(\infty,1)$-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?

Could there be a homotopified version - a realizability $(\infty, 1)$-topos?

]]>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.

]]>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 $\mathcal{E}$ such that $\Gamma\dashv\Delta$”. I call this condition “realizability-like” at one point in my thesis.

I can show that whenever $\mathcal{E}$ is a tripos-induced topos, then there exists a realizability-like $\mathcal{D}$ such that $\mathcal{E}$ is localic over $\mathcal{D}$ i.e. there exists a localic geometric morphism from $\mathcal{E}$ to $\mathcal{D}$. 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.

]]>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 : ?”

]]>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 $\mathbf{RT}(A)$ along the constant objects functor is the cocompletion of the family fibration of $A$ from finite-limit prestacks to fibered pretoposes (in the sense of my thesis). The analogy to presheaf toposes is that if $A$ is a meet-semilattice, then the gluing fibration of the presheaf topos of $A$ along $\Delta:\mathbf{Set}\to\mathbf{Psh}(A)$ is the same kind of cocompletion of the family fibration of $A$. 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 $\mathrm{Set}\to\mathbf{X}$ with exact $\mathbf{X}$, 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 $\Omega$, 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 $D$: 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 $D\to \nabla\Gamma D$ can be viewed as the internal family of all representables in the gluing fibration along $\nabla:\mathbf{Set}\to\mathcal{E}$, and $D\to 1$ is its internal coproduct.

In all the above it becomes apparent that $\nabla:\mathbf{Set}\to\mathcal{E}$ should be called $\Delta$ in a fibrational context, since it takes the role of functor along which we glue. If we call the constant objects functor $\Delta$, then $\Gamma$, being its left adjoint, deseves to be called $\Pi_0$, and we can view the situation as generalization of ‘totally connected geometric morphisms’. From this point of view, $D\to \nabla\Gamma D$ can be viewed as decomposition of $D$ into connected components.

]]>