------------- Jaap van Oosten's dissertation uses triposes to develop numerous realizability toposes, and incidentally raises the question as to which of them can be presented as the effective reflection of a category of assemblies. The answer is that all of his tripos constructions actually include constructing such assemblies. I will spell this out in some generality. Let N be any partial combinatory algebra (see Jaap's dissertation p.35). Write e.m for the result of applying an element e of N to another element m. The notation suggests the natural numbers taken as codes of partial recursive functions, but everything here works for any PCA. For any subsets W and V of N, we call an element e of N a "modulus" mapping W to V iff for every m in W the value e.m is defined and is in V. More generally, we say e maps one list of subsets W1, W2, W3... to another V1, V2, V3... iff e simultaneously maps each Wi into Vi. By a "tripos based on N" I mean a tripos such that for some subset Sub of some cartesian power of the powerset of N: 1) The fiber Sigma(X) over any set X consists of suitable pairs <alpha,t> with alpha a function from X to Sub and t coding some further structure. The pre-order says <alpha,t> is smaller than <alpha',t'> iff there is a modulus mapping alpha to alpha' and that modulus meets conditions which may depend on t and t'. 2) The action of any function f:X___>Y is by composition. Given any function from Y to Sigma, compose with f to get one from X to Sigma. For many realizabilities the tags "t" are superfluous. But in extensional realizability, for example, a member of Sigma(X) is an X-tuple of subsets of N, tagged by an equivalence relation on each one and moduli must preserve those relations. We say an element x of X is "minimally realized" by a given alpha in Sigma(X) iff alpha(x) is minimal in Sigma(1). As in any tripos we define a "relation in the sense of the tripos" on a set X to be a member of the fiber over XxX. The tripos construction of the topos works by taking as objects all pairs (X,=) where "=" is a partial equivalence relation in the sense of the tripos on the set X. The arrows are all functional relations between these pers, and the result is a topos. But in a tripos based on N we can instead take only those pairs (X,=) such that <x,y> is minimally realized by = unless x=y. These generalize the canonically separated objects in the effective topos. Together with the same arrows they form a regular category. Every partial equivalence relation on X in the sense of the tripos contains a canonically separated = such that, for any pair <x,y> non-minimally realized in the relation both <x,x> and <y,y> are non-minimally realized in =. By the soundness of tripos logic, equivalence relations and functional relations IN THE CATEGORICAL SENSE in the regular category correspond exactly to those in the tripos sense. I.e. the tripos's topos is also the effective reflection of this regular category. It only remains to note that a canonically separated = virtually is an assembly and for this special case the functional relations correspond to actual functions between carriers with moduli. A canonically separated = on X amounts to a function from X to Sigma taking each x in X to the value =<x,x>. If Sub is contained in the powerset of N then such a function gives a relation from X to N and can be given in terms of caucuses: for each n in N the n-th caucus of the assembly is the set of all x in X related to n. If Sub is contained in the I-fold cartesian power of the powerset then we get a distinct series of caucuses for each i in I. For each i we will call these the i-caucuses, so that for each n in N there is an n-th i-caucus. The tags "t" in the fibers can be kept as tags on the assemblies. The "carrier" of = is the set of all x in X with <x,x> non-minimally realized by =. A functional relation F in the sense of the tripos from (X,=) to (Y,=') amounts to an ordinary function F from the carrier of = to the carrier of =', which has a modulus. Here "modulus" means an element e of N which, for each x in the carrier of =, maps the Sigma element =<x,x> to the Sigma element ='<Fx,Fx> compatibly with the tags. In other words, let Sub be a subset of the I-fold cartesian power of the powerset of N. Then a modulus for F is a member e of N such that: for every i in I and n in N, if a member x of X is in the n-th i-caucus of = then e.n is defined and Fx is in the e.n-th i-caucus of ='; and e meets any conditions set by tags on = and ='. On his p.4 Jaap gives data for a tripos for each of some dozen kinds of realizability. His Sigma for each kind is our Sigma, and specifies what PCA each kind uses. His material implications tell which moduli are allowed. The present construction applied to his Kleene tripos gives the familiar assemblies for the effective topos. It should be clear that such assemblies and tags restricting the moduli can be described directly. On that approach, you have to show that they give a cartesian closed regular category with weak subobject classifier. That verification will be a lot like checking the Beck condition and the generic predicate in a tripos. In effect, the regular category uses the same data as the tripos only without the indexed pre-order structure. Any such regular category has a topos as effective reflection, and forms the separated objects of the topos. The method is due to Freyd and can be gleaned from Freyd and Scedrov _Categories, Allegories_. The actual statement and proof are given in Ch.25 of my _Elementary categories, elementary toposes_. Again, it is a close parallel to part of the proof that triposes give toposes, but omits much. ==============================================================================