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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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 sheaves 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).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 5th 2012

    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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeApr 30th 2014

    Added a pointer to

    and added the statement of the theorem it proves, here.

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMay 1st 2014

    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.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2014
    • (edited May 1st 2014)

    True, I have fixed it now.

    • CommentRowNumber5.
    • CommentAuthorJonasFrey
    • CommentTimeMay 1st 2014
    • (edited May 1st 2014)

    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.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2014
    • (edited May 1st 2014)

    Jonas,

    ah, thanks for fixing those glitches. Sorry.

    Regarding “closed”: for idempotent monads at least I picked this up from

    • Carboni and Janelidze and Kelly and Paré, “On localization and stabilization for factorization systems”, Appl. Categ. Structures 5 (1997), 1–58

    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.

    • CommentRowNumber7.
    • CommentAuthorJonasFrey
    • CommentTimeMay 1st 2014
    • (edited May 1st 2014)

    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 ΠΔΓ\Pi\dashv\Delta\dashv\Gamma\dashv\nabla of adjunctions, and similar ideas are relevant in realizability as well.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 1st 2014
    • (edited May 1st 2014)

    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.

    • CommentRowNumber9.
    • CommentAuthorJonasFrey
    • CommentTimeMay 1st 2014

    I added “finite-limit preserving” to “idempotent monad” since I think that’s an important property of Γ\nabla\Gamma 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.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 1st 2014

    I added “finite-limit preserving” to “idempotent monad” since I think that’s an important property of Γ\nabla\Gamma 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”.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2014

    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.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 5th 2014

    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.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 5th 2014

    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.

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 5th 2014

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

    • CommentRowNumber15.
    • CommentAuthorJonasFrey
    • CommentTimeMay 5th 2014

    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.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeMay 5th 2014

    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 DD and the “bound” of a bounded geometric morphism. I don’t suppose you have any more to say about that?

    • CommentRowNumber17.
    • CommentAuthorJonasFrey
    • CommentTimeMay 6th 2014
    • (edited May 6th 2014)

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

    In all the above it becomes apparent that :Set\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 Π 0\Pi_0, and we can view the situation as generalization of ‘totally connected geometric morphisms’. From this point of view, DΓDD\to \nabla\Gamma D can be viewed as decomposition of DD into connected components.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeMay 6th 2014

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

    • CommentRowNumber19.
    • CommentAuthorJonasFrey
    • CommentTimeMay 7th 2014
    • (edited May 7th 2014)

    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.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeMay 8th 2014

    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.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 8th 2014

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

    • CommentRowNumber22.
    • CommentAuthorJonasFrey
    • CommentTimeMay 8th 2014
    • (edited May 8th 2014)

    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 (,1)(\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?

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeMay 8th 2014

    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:

    1. lcc goes to locally cartesian closed (infinity,1)-category;

    2. exactness goes to groupoid objects in an (infinity,1)-category are effective;

    3. the faithful adjoint goes to a faithful adjoint (infinity,1)-functor.

    I am not sure what to do about the projective objects though.

    • CommentRowNumber24.
    • CommentAuthorspitters
    • CommentTimeMay 8th 2014
    • (edited May 8th 2014)

    There are two approaches:

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeMay 9th 2014

    @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 (,1)(\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.

    • CommentRowNumber26.
    • CommentAuthorJonasFrey
    • CommentTimeMay 9th 2014
    • (edited May 9th 2014)

    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 Δ:Set\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 Set\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.]

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2014
    • (edited May 9th 2014)

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

    So I understand that RT(A)RT(A) is the exact completion of PAss(A)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)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 :-)

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2014

    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?

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeMay 9th 2014

    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)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)PAss(A), I don’t think it’s necessary.

    • CommentRowNumber30.
    • CommentAuthorMike Shulman
    • CommentTimeMay 9th 2014

    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.

    • CommentRowNumber31.
    • CommentAuthorJonasFrey
    • CommentTimeMay 10th 2014

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

    1. Δ\Delta is bounded by 11 ( every AA in \mathcal{E} is a subquotient of some ΔI\Delta I)
    2. the indexed poset sub Δ\mathrm{sub}_{\mathcal{E}}\circ\Delta has a generic predicate (sub \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 :Set opCat\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

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

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

    • CommentRowNumber32.
    • CommentAuthorJonasFrey
    • CommentTimeMay 10th 2014

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

    • CommentRowNumber33.
    • CommentAuthorJames Francese
    • CommentTimeApr 18th 2019

    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.

    • CommentRowNumber34.
    • CommentAuthorspitters
    • CommentTimeApr 18th 2019
    • (edited Apr 18th 2019)

    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.

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2019

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

    diff, v21, current

    • CommentRowNumber36.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 16th 2019

    This seems to be described also at partial combinatory algebra.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeJun 16th 2019

    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.

    diff, v22, current

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeJun 17th 2019

    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.

    • CommentRowNumber39.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 17th 2019

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

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeMar 29th 2021

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

    diff, v23, current