{'fraction_non_alphanumeric': 0.0604089219330855, 'fraction_numerical': 0.006195786864931847, 'mean_word_length': 3.8216152779259573, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 29, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Categories of assemblies for realizability

This paper introduces categories of assemblies which are closely connected to realizability interpretations and which are based on an important subcategory of the effective topos. There is a list of properties which characterize these categories of assemblies up to equivalence.


Introduction
The many techniques aggregated in realizability demonstrate the consistency of certain classically false statements with non-classical logics, in particular with intuitionistic logic. This paper charts the capabilities of realizability by categorical means.
This paper is about a class of categories which generalize the category of assemblies (see below) which is equivalent to the category of ¬¬-separated objects of the effective topos. Each generalized category of assemblies is a Heyting category (theorem 30). Each category of assemblies implicitly defines a realizability interpretation of its internal language, such that valid and realized propositions coincide (theorem 33). The latter half of this paper outlines some structure and properties which determine when an arbitrary category is equivalent to a category of assemblies (theorem 49).
The motivating example of this paper is the category of assemblies. Informally an assembly a is a non-classical subset of an arbitrary set s. For each x ∈ s, a set of natural numbers witnesses the membership of x to a. These numbers are the realizers of x ∈ a. For each subassembly a ′ of each set s ′ and for each function f : s → s ′ , partial recursive functions determine whether the restriction of f to a factors through a ′ . Formally, this is defined as follows.
Definition 1. An assembly is a pair (X, α) where X is a set and α is a function X → PN valued in nonempty subsets of N.
Let (X, α) and (Y, β) be two assemblies. A total morphism (X, α) → (Y, β) is a function f : X → Y which has a partial recursive g : N ⇀ N such that for each x ∈ X and n ∈ α(x), n is in the domain domg of g and g(n) ∈ β(f (x)).
Assemblies and total morphisms together form the category Asm of assemblies.
The category of assemblies is closely related to the effective topos of Hyland [8,15,22]. On one hand Asm is equivalent to the subcategory of ¬¬-separated objects of the effective topos and on the other hand the effective topos is the ex/reg completion of Asm, i.e. the result of freely adding quotients to internal equivalence relations in a way that respects regular epimorphisms [2,3,[13][14][15]. I choose to discuss the category of assemblies rather than its ex/reg completion, because its properties are more stable. This paper generalizes the category of assemblies along two lines. Firstly, different sets of realizers and computable functions replace the natural numbers and partial recursive functions. Secondly, the object and morphisms of other categories replace sets and functions. The following conditions confine the generalizations this paper presents.
• The base category is a Heyting category (see definition 2). • All notions of computability are Turing complete.
• There are no order partial combinatory algebras [7,22] other than partial combinatory algebras in this paper. • There is no additional structure on the object of realizers in this paper, as found in modified and extensional realizability [10,[20][21][22].
Weaker than Turing complete notions of computability can still give interesting realizability categories as the following papers show: [5,6,11]. The approaches in these papers are limited by what can either be seen as an extra constraint on the base category (a projective terminal object) or a different constraint on the notion of computability (inhabited families of computable function have at least one computable global section). This paper shows how to overcome these limitations, but only for the special case Turing complete computability. The other constraints are also aimed at keeping things simple, although I have developed a lot of theory for order partial combinatory algebras elsewhere [17,18].
This paper omits theory on functors between categories of assemblies and to other categories. Much of this can be found in my other work [17,18]. There are straightforward generalizations of Longley's applicative morphisms [12] which are a useful tool for studying regular 19 functors between realizability toposes. Hofstra and Frey generalize these in [5,6] for other realizabilities. The reason I do not get deeper into these right now, is that there is a notion of applicative morphism related to finite limit preserving functors between realizability toposes (the left exact morphisms in [17]) which I am exploring for another paper.
The characteristic properties of realizability categories are formulated as a list of axioms in this paper (axioms 34, 37 and 38). They may be translated in the internal language of the categories with some extra effort, to give an axiomatization of realizability like Dragalin's [4] and Troelstra's [19]. I have outlined the possibilities in my thesis [17], but this extra effort will have to wait for another paper too.
I have avoided realizability triposes and similar structures throughout this paper. This should make the content accessible to readers who are unfamiliar with categorical realizability. However, familiarity with categorical logic is not a luxury.

Ingredients
The generalized categories of assemblies look like this: the objects and morphisms of an arbitrary Heyting category replace set and functions; some object A replaces N; partial morphisms A ⇀ A which are φ-computable relative to a partial application operator · : A × A ⇀ A and a combinatory complete filter φ, replace the partial recursive functions. This section defines what the emphasized words in the previous sentence mean.
2.1. Heyting categories. Heyting categories correspond to theories in many sorted first order intuitionistic logic. Theories induce Heyting categories of definable functions and Heyting categories have an internal language which is a many-sorted first order intuitionistic logic.
Definition 2 (Heyting category). Let C be any category. For each object X of C, a subobject is an isomorphism class of monomorphisms into X. Factorization induces a partial order ⊆ on subobjects. The poset of all subobject is Sub(X). If C has all pullbacks, then for each morphism f : X → Y pulling back monics induces a function f −1 : Sub(Y ) → Sub(X) called the inverse image map.
A Heyting category is a category where the poset of subobjects Sub(X) is a Heyting algebra for each object X and where the inverse image map of each arrow is a homomorphism of Heyting algebras which has both adjoints. This means that • for each object X, Sub(X) has finitary joins (∅, ∪), finitary meets (X, ∩) that distribute over joins and a map d : Example. Every topos, including the category of sets and the effective topos is a Heyting category. In fact all regular (see definition 19) extensive locally Cartesian closed categories, like the category of assemblies from the introduction, are Heyting.
Heyting algebras admit an interpretation of a propositional language for which intuitionistic propositional logic is sound. The rest of the structure handles the extension to first order logic. The inverse image map takes care of substitutions. The adjoints take care of quantification and equality. The Beck-Chevalley condition says that quantification commutes with substitution. Definition 3. First order logic defines subobjects of objects in Heyting categories. I regularly exploit this in the definitions below. The following notation sets the formulas and subobjects of the internal language apart form the formulas and sets of the metalanguage: • For u ∈ Sub(X), is the related predicate is denoted x:u.
• For each formula χ with no other free variables than x of type X, x:X|χ(x) defines the related subobject of X.
Definition 4 (Representative monomorphisms). There is little harm in only considering small categories, because by Gödels completeness theorem there are small models of set theory. This makes Sub(X) a large set of large sets instead of a proper class of proper classes. The advantage is that for each small category with finite limits, there is a function that chooses for each object X and each subobject U ∈ Sub(X) a monomorphism µ U : X U → X by the axiom of choice. Such representative monomorphisms figure in proofs throughout this paper.

2.2.
Partial combinatory algebras. The starting point for the model of computability is the universal computer: this is a device that takes a string of code and an string of input, performs a computation and produces a string of output provided that the computation terminates. The following structure captures this idea inside a Heyting category.
Definition 5 (Partial applicative structure). Let B be a Heyting category. A partial applicative structure is a pair (A, ·) where A is an object and · is a partial morphism A × A ⇀ A. Here, a partial morphism X ⇀ Y is an isomorphism class of spans (m : Z → X, f : Z → Y ) in which m is monic. I refer to · as the application operator.
The desired model of computation allows computable functions to work on noncomputable data and therefore permits subobjects of A to exclude computable elements. The following structure 'filters' those non-computable subobjects out.
Definition 6 (Filter). Let B be a Heyting category and let A be a partial applicative structure in B. A filter is a subset φ ⊆ Sub(A) with the following properties.
• If U ∈ φ, then U is inhabited, i.e. the canonical map form A U to the terminal object 1 is a regular epimorphism.
Example. The set of inhabited subobjects is a filter. If C ⊆ A is a subobject such that for all x, y ∈ C, if (x, y):dom(·) then x · y ∈ C, then the set of subobjects that intersect C -i.e. U ∩ C is inhabited -is a filter.
Computability means 'having a computable code on the universal machine' and is therefore formalized as follows.
Definition 7 (Computable). Let B be a Heyting category, let A be a partial applicative structure in B and let φ be a filter on A. For each n ∈ N an n-ary partial morphism f : A n ⇀ A is φ-computable if there is an R ∈ φ such that • for all r ∈ F and x ∈ A n−1 , ((r · x 1 ) · · · x n−1 ) is defined • for all r ∈ F and y ∈ domf , ((r · y 1 ) · · · y n ) is defined and equal to f ( y) Both of these statements should be interpreted in the internal language of B. Therefore let a 1 : A → A be the identity and let a n+1 : A n+1 ⇀ A for n > 0 satisfy: dom(a n+1 ) = (a n × id) −1 (dom(·)), a n+1 = (·) • (a n × id) The reformulation is: ) and a n+1 restricts to f • π 1...n where π 1...n is the projection F × domf → domf The following condition ensures that φ-computability has enough power to realize the soundness of first order logic.
Definition 8 (Combinatory completeness). Let B be a Heyting category, let A be a partial applicative structure in B and let φ be a filter on A. The filter φ is combinatory complete if all projections x → x i : A n → A are φ-computable and if φ-computable maps are closed under pointwise applications, i.e. if f : A n ⇀ A and g : A n ⇀ A are φ-computable, then (·)•(f, g) : Example. There is a universal partial recursive function · : N × N ⇀ N. The filter of inhabited subobjects is combinatory complete for the applicative structure (N, ·). This holds for each natural number object in each Heyting category.
The following structures connect applicative structures to combinatory logic [16].
Definition 9 (Partial combinatory algebras). A partial combinatory algebra is a partial applicative structure (A, ·) with inhabited k, s ∈ Sub(A) that satisfy: • for all k ∈ k and x, y ∈ A, (k · x) · y = x.
• for all s ∈ s and x, y ∈ A, (s · x) · y is defined.
Theorem 10. A partial applicative structure (A, ·) is a partial combinatory algebra if and only if it has a combinatory complete filter.
Proof. Let φ be a combinatory complete filter on (A, ·). The morphisms (x, y) → x and (x, y, z) → (x · z) · (y · z) are computable by combinatory completeness. Hence there are suitable k and s ∈ φ. Since members of φ are inhabited (A, ·) is a partial combinatory algebra. Converse: the filter of inhabited subobjects of A is combinatory complete, because the combinators k and s form a complete basis for combinatory logic (see [16]).
Remark. The definition of computability says that as long as some parts of the input of a computable function are missing, the universal computer makes a computation which always halts. This is realistic, as a real computer can just store input and only start computing when every bit of input is collected. Without this property of computability, the combinatory complete filters are connected to conditional partial combinatory algebras [9], which are equivalent to ordinary partial combinatory algebras for realizability (by proposition 1.2.3 of [22]), but harder to use.

2.3.
Computability. This subsection contains technical results for the proof that the generalized categories of assemblies are Heyting categories. That proof is essentially the soundness theorem of first order intuitionistic logic for realizability interpretations. This section defines certain relations on partial applicative structure with the help of the λ-calculus [1], and demonstrates that these λ-definable relations contain φ-computable morphisms for any filter φ.
The λ-calculus describes a set of functions that act on each other. They determine a notion of computability that is equivalent to Turing computability. The βη-conversion relation is the least preorder → βη on λ-terms that satisfies: Remark. This definition highlights properties of βη-conversion that are convenient in this context. Ordinarily, → βη is defined as the least preorder that satisfies: The proof that these conditions define the same relation is an exercise for the reader. See [1] for more λ-calculus.
Any partially ordered set P with monotone maps α : P → P P and λ : P P → P such that α ⊣ λ allows and interpretation of λ-terms which respects βη-conversion.
Here the fibred poset Sub(− × A) plays the role of P in the following manner. The sets Sub(X × A × A) represent certain functions Sub(X × A) → Sub(X × A), namely functions of the following form.
Here (and from now on) ∃(x, a):U.χ is short for ∃(x ′ , a):U.x = x ′ ∧χ. An adjunction between Sub(A) and Sub(A × A) determines a lax kind of model of the λ-calculus. Informally, the adjunction comes from the inverse and direct image maps of the 'function': The following formalizes this in a Heyting category without power objects.
Definition 12. Form now on, let x · y↓ stand for (x, y):dom(·). For each object X of B and each U ∈ Sub(X × A) and V by assumption and α X (U ) ⊆ V follows by generalization.
Let me show how the fibred adjunction α X ⊣ λ X satisfies → βη .
For each λ-term M the set of free variables FV(M ) is defined as follows: For each n ∈ N interpret the λ-terms M with #M < n as follows: Lemma 15. For each n ∈ N and each pair of λ-terms M, N such that #M , Proof. This is a proof by nested induction, namely induction over the rules that define substitution inside induction over the rules that define conversion. The following equality holds by induction over the substitution rules: I extend the possibilities for defining relations with the λ-calculus a little bit further. The lemmas above generalize to the extended language without trouble.
Definition 16. A λ-term with constants is a λ-term which besides variables has elements of Sub(A) as atomic subterms. The set of λ-terms with constants is Λ Sub(A) . For U ∈ SubA, let FV(U ) = ∅ and for each n ∈ N let [[U ] ] n = A n × U .
To simplify notation, I use to following conventions: • • Application has priority over abstraction and associates to the right, so λx, y, z.xyz = λx, y, z.((xy)z). The end of this subsection is about λ-definable subobjects of A that are members of any combinatory complete filter φ. Let me explain why not all λ-definable subobjects are elements of every filter. If U, V ∈ φ, then U V is a λ-term with constants and which is in φ simply because there are computable morphisms and φ is upward closed. It is unclear what happens when ∀u:U, v:V.u · v↓ is undecidable. Therefore φ may exclude [[U V ]]. It turns out that combinatory complete filters only bar applications, however.
Lemma 17 (Computable terms). Let Λ φ be λ-terms whose constants are in φ. Let M ∈ Λ φ such that FV(M ) = ∅ and such that M is not the application of two other λ-terms.
Proof. Since M has no free variables and is no application, it is either a constant in φ or an abstraction. If M ∈ φ, then [[M ]] = M ∈ φ by assumption. This leaves the case that N is an abstraction. If M is an abstraction, then is it of the form λx 0 , · · · , x n .N (for arbitrary n) where either N = x i for some i ≤ n, N ∈ φ or N = P Q for some other λ-terms P , Q.
∈ φ for the following reason. Repeated application determines the following families of computable functions: The last family is the pointwise application of the first two.

Categories of assemblies
This section generalizes the definition of the category of assemblies in the introduction, replacing sets, functions and partial recursiveness with objects and morphisms from a Heyting categories and partial computable morphisms. I have to make two adjustments. Firstly, assemblies are bundles of subobjects of A, because the power object PA may be absent from B. Secondly, inhabited families of computable morphisms rather than individual morphisms determine which morphisms between assemblies are total.
Definition 18 (Category of assemblies). Let B be a Heyting category, let (A, ·) be a partial combinatory algebra of B and let φ be a combinatory complete filter of (A, ·). An A-assembly is a pair (X, ξ) where X is an object of B and ξ is a member of Sub(A × X) that satisfies: For each assembly X = (Y, Φ) let UX = Y and ρ X = Φ in order to save variables.
Let X and Y be assemblies The φ-total morphisms are closed under composition and identities because computable functions are. The category of assemblies Asm(B, (A, ·), φ) consists of A-assemblies and φtotal morphisms.
An A-assembly X is a fresh subobject of the object UX in B whose membership is determined by the relation ρ X . A morphism between underlying object is φtotal, if there are φ-computable morphisms to take care of the realizers. This is all parallel to how the ordinary category of assemblies was defined. In fact, that category is an example.
Example. If S is the category of sets, · : N × N ⇀ N a universal partial recursive function and if φ is the filter of inhabited subobjects of N, then Asm(S, (N, ·), φ) and the category of assemblies of definition 1 are equivalent.
Remark (Alternative). Spans (a : Y → A, x : Y → X) represent every subobject in Sub(A × X) at least once. For this reason, there is an equivalent category whose objects are spans and whose definition is less dependent on an ambient set theory or on the internal language of B. Such a definition makes the proof that the category of assemblies is a Heyting category much more complicated, however.
3.1. Regularity. The rest of this section is a tedious check that categories of assemblies are Heyting categories. This subsection goes halfway with a proof that A regular epimorphism is a morphism that is the coequalizer of its own kernel pair. A C is regular if regular epimorphisms are stable under pullback and if each kernel pair has a coequalizer.
A functor between regular categories is regular if it preserves finite limits and regular epimorphisms.
Example. Categories of algebras and homomorphisms are usually regular. So are all toposes.
Upcoming proofs require the following properties of regular categories and functors.
Definition 20. For each f : X → Y in a regular category, and each monic m : W → X, f • m factors into a regular epimorphism followed by a monomorphism in an up to isomorphism unique way. Since this factorization preserves isomorphisms between monomorphisms, it induces a function Sub(X) → Sub(Y ), which equals the direct image map in Heyting categories. Hence I denote it by ∃ f .
has a left adjoint ∃ f which satisfies the Beck-Chevalley condition. Each regular F : C → D be a regular functor preserves monomorphisms and therefore induced family of morphisms F X : Sub(X) → Sub(F X), which commutes with all inverse image maps and all of their left adjoints.
Proof. This proof is left as exercise for the reader.
Definition 22. The following operators construct assemblies with useful properties.
• For every object X of B, ∇X = (X, A × X).
Assemblies of this form have the property that each morphism UY → X determines a φ-total morphism Y → ∇X. In particular id UY : Y → ∇UY is φ-total for each assembly Y .
• For every assembly Y and every f : X → UY let: The important property of this construction is that f The reason is that if R ∈ φ tracks one, it automatically also tracks the other.
• For every assembly X and every regular epimorphism e : UX → Y let: This construction is dual to the last: its property is that f • e : X → Z is φ-total if and only if f : e * (X) → Z is. The reason that this only works for regular epimorphisms, is that each assembly Y has to satisfy B |= ∀x:UY.∃a:A.ρ Y . Note that e * e * (Y ) = Y : because id A × e is a regular epimorphism, • For every pair of assemblies Y and Y ′ for which UY = UY ′ = X let: In this case, Y ⊗ X Y ′ is the pullback of the canonical morphisms id X : Y → ∇UY and id X : Y ′ → ∇UY ′ for the following reasons. The mor- x(λy, z.y)]] and [[λx.x(λy, z.z)]] ∈ φ. Of each pair of φ-total morphisms p : Z → Y and q : Z → Y ′ such that id UY • p = id UY • q the underlying maps are equal. Finally, if U ∈ φ tracks p : Note that for each f : Remark. It may please readers familiar with fibred categories to know that the underlying object map is a fibred bounded meet semilattice. It has supine morphisms over all the regular epimorphisms and because these supine morphisms are prone, U is also a stack for the regular topology of B (see [23] for more stacks).
This demonstrates that Asm(B, (A, ·), φ) has finite limits. The functor ∇ preserves these limits because it is a right adjoint to U. The construction of finite limits above show that limits in Asm(B, (A, ·), φ) lie direct above limits in B. Hence U preserves finite limits too.
Concerning regular epimorphisms: let f, g : X → Y be a parallel pair of φ-total arrows which have a coequalizer e : UY → Z in B. Since e is a regular epimorphism, e * (Z) is an assembly. Suppose h : The following shows that this e ′ is a regular epimorphism because e ′ * ((e ′ ) * (Y ) ⊗ W (f ′ ) * (X)) is isomorphic to Y . One can verify the following equations by raw computation The φ-total morphism id UZ : e * (X) → Z is an isomorphism because e : X → Z is a coequalizer for the same kernel pair as e : X → e * (X). The operator f * preserves this isomorphism, so f * (e * (X)) and f * (Z) are isomorphic. The morphism ) is isomorphic to Y , e ′ is a regular epimorphism. By generalization all regular epimorphism are stable under pullback.

3.2.
Soundness. This subsection holds the proof that the category of assemblies is a Heyting category. This means that intuitionistic logic is sound for realizability interpretations which are connected to categories of assemblies. To complete the proof that Asm(B, (A, ·), φ) is a Heyting category, I first demonstrate the equivalence of the subobject lattices in categories of assemblies with simpler preordered sets.
Definition 24. For each object X of B and U, V ∈ Sub(A × X), let Note that | Here µ U : X U → X is the monomorphism in U chosen in definition 4.
Lemma 26. The map E X determines an equivalence between Sub(X) and the initial segment [∅, ρ X ] of (Sub(A × UX), | r =).
Proof. Suppose that U, V ∈ Sub(X) and U ⊆ V . There is a unique monic p : This means that the pullback n : W → X U of µ V along µ U is a regular epimorphism. Because U preserves finite limits, it preserves pullbacks and monomorphisms. Hence n is an isomorphism. If m is the pullback of µ U along µ V and p = m • (n) −1 then µ V • p = µ V as required. This proves that E X is full and faithful.
A.υ(a, x) and let µ U : UX U → UX be the monomorphism that represents it (as in definition 4). The pair (U, (id A ×µ U ) −1 (υ)) is an assembly and µ U : There is a V ∈ SubX such that µ V is isomorphic to µ U as monomorphism in Asm (B, (A, ·), φ)). Hence E X is essentially surjective. By the axiom of choice, E X has a weak inverse functor and is an equivalence of categories.
Proof. Due to the equivalence E X , Sub(X) is a Heyting algebra if [∅, ρ X ] is a biCartesian closed preordered set. I prove the latter statement.
It is easy to see that [∅, ρ X ] has a top and bottom element. Because Asm(B, (A, ·), φ) is regular, Sub(X) has binary meets. I give a proof that binary meets exist in [∅, ρ X ] because it helps to define Heyting implication later on. Remember that the interpretations of many λ-terms are members of φ by lemma 17. One of those is the following p = λx, y, p.pxy The following λ-terms help to define binary joins.
Hence U | All the required structure is present in [∅, ρ X ]. Therefore Sub(X) is a Heyting algebra.
The next lemma says that the inverse image map of any φ-total morphism f : Proof. Naturalness is the easy part of this lemma, because [∅, ρ X ] is a preordered set and every square in it is commutative. That leaves the problem of finding the isomorphisms.
For each U ∈ Sub(Y ), let µ U : Y U → Y be its representation. The following equations hold by definition.
There is a unique morphism g : X f −1 (U) → Y U such that the morphism f , µ f −1 (U) , µ U and g form a pullback square.
The universal property of the g * construction (see definition 22) makes g * (Y U ) another assembly over UY U for which this square is a pullback. Hence g * (Y U ) ≃ X f −1 (U) and The Beck-Chevalley condition in B implies: Since this construction works for arbitrary subobjects, the inverse image map f −1 in Asm (B, (A, ·), φ) commutes up to isomorphism with (id A × f ) −1 in B.
The following lemma completes the proof that Asm (B, (A, ·), φ) is a Heyting category.
Lemma 29. Let f : X → Y be a morphism of Asm (B, (A, ·), φ). Its inverse image map f −1 is a morphism of Heyting algebras, it has both adjoints ∃ f ⊣ f −1 ⊣ ∀ f and these adjoints satisfy the Beck-Chevalley conditions.
Proof. If f −1 preserves Heyting implication and has a right adjoint, then the rest of the properties hold for the following reasons. In every regular category, f −1 has a left adjoint which satisfies the Beck-Chevalley condition. That the left adjoint satisfies the Beck-Chevalley condition implies that the right adjoint does too. A functor that has both adjoints preserves all limits including all finitary meets and joins of the Heyting algebra. The rest of this proof shows that (id ρ X ] has a right adjoint and preserves implication, so that the inverse image map does too. There already is an adjunction between (id A × f ) −1 and ∀ idA×f relative to the inclusion orders ⊆ on Sub(A×UX) and Sub(A×UY ). Because α ⊆ β implies α | r = β on either side; because (id A × f ) −1 preserves | r =, this adjunction is preserved. Write out the definitions in order to see that The main theory of this subsection is a straightforward corollary of the lemmas above: Theorem 30. For each Heyting category B, each partial applicative structure (A, ·) of B and each combinatory complete filter φ, the category of assemblies Asm (B, (A, ·), φ) is a Heyting category.
Remark (Realizability toposes). By the way, realizability toposes are ex/reg completions of specific categories of assemblies. The ex/reg completion C ex/reg of a regular category C freely adds quotients of internal equivalence relations, while preserving regular epimorphism in C. The construction is a left biadjoint to the inclusion of regular categories and regular functor into the category of exact categories and regular functors [2,3,15]. I have studied the properties of ex/reg completions of categories of assemblies in [17,18]. The category Asm(B, (A, ·), φ) ex/reg is a topos if B is, because in that case Asm(B, (A, ·), φ) has a generic monomorphism (see [13,14]).

3.3.
Realizability. The category of assemblies are a tool for studying many forms of realizability. This section shows how to connect a realizability interpretation to a category of assemblies.
As in ordinary categorical logic, the internal language of a category of assemblies assigns subobjects of its terminal object to each proposition. The lattice of subobjects of 1 in Asm (B, (A, ·), φ) is equivalent to the poset (Sub(A), | r =) in B by lemma 26. Thus the category of assemblies assigns an equivalence class of subobjects of A to each proposition. Realizability makes these choices inductive on subformulas.
Definition 31 (Realizability). I recursively define the formula a r p, where p is a formula of the internal language of Asm(B, (A, ·), φ) and a is a variable symbol of type A. This is called the realizability relation. The realizability of atomic relations, which come form subobjects U ⊆ X in Asm(B, (A, ·), φ) is determined by a choice between the representations that U has in [∅, ρ X ]. For the chosen V ⊆ A × UX realizability is defined as follows: a r x:U ⇐⇒ (a, x):V The realizability interpretation satisfies a proposition p if a:A|a r p ∈ φ.
Remark (Diversity). The definitions of ∀, → and validity impose a preorder on formulas, which forms a Heyting algebra in sound realizability interpretations. This determines how the rest of the logic is realized up to equivalence. So even though realizability interpretations in the literature may differ in the details, they often satisfy the same propositions.
Lemma 32. Let p be a proposition in the internal language of Asm(B, (A, ·), φ) and let τ p ∈ Sub(1) be its truth value. Then a:A|a r p is equivalent to E 1 (τ p ).
Proof. Left as exercise.
Theorem 33. Let p be a proposition in the internal language of Asm(B, (A, ·), φ) and let τ p ∈ Sub(1) be its truth value. Then τ p = ⊤ if and only if the realizability interpretation satisfies p.
Proof. The equivalence of E 1 (⊤) and a:A|a r p means that one is in φ if the other is, but E 1 (⊤) = A ∈ φ.
Categories of assemblies are connected to an internal form of realizability in arbitrary Heyting categories. The filters add a lot of flexibility.
• Ordinary realizability interpretations satisfy every formula that has realizers. This corresponds to the filter of inhabited subobjects of a partial combinatory algebra. • The correct interpretation of 'having realizers' may be that the set of realizers has a global section, however. In that case the filter set of subobjects of A which have a global section determine the category of assemblies. • In relative realizability, A has a subset A ′ of special realizers and a proposition is valid if it has a realizer in A ′ . Having realizers can refer to either inhabited subobjects or to global sections. In the first case A ′ is a subobject of A and the filter is the set of subobject that intersect A ′ . In the second case A ′ is a set of global section and the filter is the set of subobjects through which some of these globals sections factorize.
• Filters are closed under intersections and hence realizability interpretations are too. This is a new construction for realizability models as far as I know. Thus categories of assemblies cover a lot of ground as far as realizability in concerned.

Realizability categories
This section contains a characterization of the categories that are equivalent to a category of assemblies. Later sections explain to what extend and how the characteristic properties of these categories can be expressed in their internal language. The definition involves some extra structure of Asm(B, (A, ·), φ) for the following reason. In any Heyting category B the terminal object 1 and the unique map ! : 1 × 1 → 1 form a partial applicative object and {1} is combinatory complete filter. In this case U : Asm(B, (1, !), {1}) → B is an equivalence of categories. This means that every Heyting category is a realizability category in a trivial way.
The following extra structure is taken in consideration. The category of assemblies Asm (B, (A, ·), φ) extends the category B with new subobjects. There is a special new subobjectÅ (which is introduced in definition 39) which generates all others in some sense. The definition of realizability category characterizes the combination of the inclusion ∇ : B → Asm(B, (A, ·), φ), the underlying object functor U and this assemblyÅ.
Throughout this section, let B and C be Heyting categories let F : B → C and U : C → B be two functors, and let C be some object of C.
Axiom 34 (Separability). The functor F is right adjoint to U . Both functors are regular. The unit η : id C → F U is a natural monomorphism. The co-unit ǫ : U F → id C is a natural isomorphism.
Remark. I call this the separability axiom because U is a kind of fibred category. To be precise The axiom forces U to be a Street fibration, i.e. the composition of a Grothendieck fibration and an equivalence of categories. More relevantly, the axiom also tells us that the Grothendieck part is separated relative to the regular topology on B.
The following definition helps to formulate the next axiom, which says that every object is an assembly.
The following characterization of prones is very useful in this context.

Proof. Left as exercise.
Axiom 37 (Weak genericity). For each object X of C there is a span p : Y → C, e : Y → X where p is prone and e is regularly epic.
Remark. For an ordinary fibred category U : C → B a generic object is an object G of C such that there is a prone morphism X → G for every object X of C. The object G the axiom only generates a cover for each object of C, i.e. it is only weakly generic. This is why I call this axiom the weak genericity axiom.
The last axiom says that every morphism is φ-total for the filter of R ⊆ U C for which F R intersects C.
Axiom 38 (Tracking). There is a partial operator · : C × C ⇀ C for which the inclusion dom(·) ⊆ C × C is prone and which has the following property. Let f = (f 0 , f 1 ) : Y → C×X be a monic such that f 1 : Y → X is a regular epimorphism, let p : P → C be prone and let g : P → X. There is an inhabited R ⊆ C such that r · p(x)↓ for all x:P and (r, x) → (r · p(x), g(x)) factors though f .
The upcoming subsection explains why Asm(B, (A, ·), φ) is a realizability category. The one after that shows that for every category that satisfies these axioms there is an equivalent category of assemblies.

4.2.
Satisfaction. This subsection demonstrates that Asm(B, (A, ·), φ) satisfies the axioms in the previous subsection for any partial applicative structure (A, ·) in B and any combinatory complete filter φ. Theorem 23 says that axiom 34 holds if F = ∇ and U = U. I now formally introduce the assemblyÅ which takes the place of C in each category of assemblies.
Definition 39. Let (A, ·) be a partial applicative structure and let φ be a combinatory complete filter. LetÅ be the diagonal assembly (A, (a, a):A × A|a:A ).
The next theorem justifies axiom 37.
Theorem 40 (Weak genericity). For each assembly X of Asm(B, (A, ·), φ) there is an assembly Y with a prone morphism p : Y →Å and a regular epimorphism e : Y → X.
The following lemma explains the role of the filter φ.
Lemma 41. For all I ∈ SubA, ∇I ∩Å is inhabited if and only if I ∈ φ.
Theorem 42 (Tracking). There is a partial morphism ▽ :Å ×Å ⇀Å for which the inclusion dom▽ →Å ×Å is prone that has the following property. Let f = (f 0 , f 1 ) : Y →Å × X be a monomorphism, such that f 1 is a regular epimorphism. Let p : P →Å be prone and let g : P →Å be an arbitrary morphism. There is an inhabited R ⊆Å such that r · p(x)↓ and (r, x) → (r(x) · p(x), g(x)) factors through Y .
I use some of the operators of definition 22 now. Because p : P →Å is prone, Since no generality is lost, assume P = p * Å and X = (f 1 ) * (Y ). There is an I ∈ φ that tracks g : p * Å → (f 1 ) * Y and a J ∈ φ that tracks f 0 : Y → C. Let Under these circumstances for each r:I •J and x:UP , there is unique y:UY such that g(x) = f 1 (y) and r • p(x) = f 0 (y). Therefore there is a morphism h : (J • I)× UP → Y such that f 1 • h = g • π 1 and f 0 (h(r, x)) = r · p(x). Let R =Å ∩ (J ⊗ I). There is a K ∈ φ that tracks g • π 1 : R × P → X. This K also tracks h : R × P → Y , which is therefore a φ-total morphism. The object R is an inhabited subobject of A. Therefore the tracking axiom applies to categories of assemblies.
The axioms of realizability categories are sound for categories of assemblies. The next subsection tackles completeness. 4.3. Characterization theorem. The last subsection explained why categories of assemblies are realizability categories. This subsection explains why every realizability category is equivalent to a category of assemblies.
Throughout this subsection let Heyting categories B, C, functors F : B → C, U : B → C and an object C of C satisfy the axioms for a realizability category. Let A = U C, let · : A × A ⇀ A equal U (·) : U C × U C ⇀ U C and let φ contain those subobjects S of A such that F S intersects C. This subsection demonstrates that there is an equivalence G : Asm(B, (A, ·), φ) → C which satisfies G∇ ≃ F and GÅ ≃ C. I first define an object map for the equivalence. Because Let GX be F UX Ξ(X) and let g X = µ Ξ(X) : GX → F UX (µ from definition 4).
There is an R ∈ φ that tracks f : X → Y . For each (c, x):F (ρ X ) and r:F R ∩ C, r · c↓ and (r · c, F f (x)):F (ρ Y ) because R tracks f and r · c:C because C is closed under application. For this reason, the restriction of F f to Ξ(X) factors through Ξ(Y ) and that means there is a map h : Lemma 46. The maps G form a functor Asm(B, (A, ·), φ) → C which satisfies G∇ ≃ F and GÅ ≃ C.
Proof. The arrow map G preserves composition and identities for the following reason. For any chain of arrows {f i : By lemma 44, Gf n−1 • · · · • Gf 0 = G(f n−1 • · · · • f 0 ) and therefore G is a functor.
The functor G now satisfies G∇ ≃ F for the following reason. For each X in B, Ξ(∇X) = x:F X|∃c:C.(c, x):F A × F X Therefore g X : G∇X → F X is an isomorphism. ForÅ, Ξ(Å) = a:F A|∃c:C.c = a For this reason GÅ is isomorphic to C.
Both categories C and Asm(B, (A, ·), φ) satisfy the weak genericity axiom, but in Asm(B, (A, ·), φ) each object X has a prone-regularly-epic span p : Y → A, e : Y → X where (p, e) : Y → A × X is monic. Proving that G is an equivalence becomes simpler after proving that C has jointly monic prone-regularly-epic spans too.
Lemma 47 (jointly monic spans). For each object X of C, there is a jointly monic prone-regularly-epic span p : Y → A, e : Y → X.
Proof. By weak genericity, there is a prone-regularly-epic span q : Z → A and f : Z → X. The morphism (q, f ) : Z → A × X factors as a regular epimorphism e ′ : Z → Y followed by a monomorphism (p, e) : Y → A × X. The morphism e : Y → X is regularly epic because e • e ′ = f and both e ′ and f are regularly epic. Morphism p is prone for the following reasons. For each regular epimorphism r : P → Q in C the naturalness square of r and the unit η : id C → F U is a pullback, because F U preserves regular epimorphisms and η is monic and because every square with vertical regular epimorphisms and horizontal monomorphisms is a pullback square. P Therefore every regular epimorphism is a prone morphism. It is easy to see that prone morphisms satisfy 2-out-of-3 using lemma 36, so because p • e ′ = q and both e ′ and q are prone, so is p.
Proof. The reasons that G is essentially surjective on objects are the following. Weak genericity says that for each object Y of C, there is a span consisting of a regular epimorphism e : Z → Y and a prone morphism p : Z → C. Using one of these spans, define the assembly HY as follows: With Ξ from definition 43 regularity of F and U implies that: Because p : Z → C is prone, the naturalness square of the unit η : id C → F U and p is a pullback by lemma 36: is an element of the subobject z:F U Z|c = F U p(z) . The subobject Ξ(HY ) is just ∃ F Ue (Z), but this subobject contains the monic η Y : Y → F U Y , because it is the monic part of an regularly-epic-monic factorization of F U e • η Z by naturalness of η.
, so they are isomorphic. Hence G is essentially surjective on objects.
Concerning faithfulness: by definition U C = A. Since U is a regular functor, The isomorphism ǫ : U F → id B together with the definition of A-assembly imply that the transpose g t : U G → U is a natural isomorphism. Since U is faithful, so is G.
Fullness of G relies on tracking. For each assembly X let the monomorphism (p X , e X ) : R X → C × GX represent the following subobject: (c, x):C × GX|(η C (c), g X (x)):F A×UX (ρ X ) This way p X : R X → C and e X : R X → GX is a jointly monic prone-regularly-epic span for GX.
Let Y be another assembly and let h : GX → GY be any map. These morphisms satisfy the conditions of the tracking axiom: (p Y , e Y ) : R Y → C × GY is a monomorphism, e Y : R Y → GY is an epimorphism, p X : R X → C is prone and there is a map h•e X : R X → GY . So there is an inhabited S ⊆ C such that s·p X (r)↓ for all r:R X and s:S and such that there is a morphism t : S × R X → C × R Y that satisfies t 0 = (·) • (id S × p X ) and t 1 = h • e X • π 1 factors through (p Y , e Y ).
Because the inclusion of the domain of the application operator is prone, (s·r) → s · p(r) defines a map C ∩ F U S × R X → C. Because p Y : R Y → C is prone too, there is a unique extension of t to C ∩ F U S × R X . The object U S belongs to φ because S ⊆ C ∩ F U S and S is inhabited.
The transpose g t : U G → U is an isomorphism. Hence there is a unique h ′ : UX → UY commuting with U h : U GX → U GY . This h ′ is φ-total since U S ∈ φ. Finally, Gh ′ = h by definition of G.
By generalization the content of this subsection summarizes as the following theorem.
Theorem 49 (Characterization). Let B and C be Heyting categories, let F : B → C and U : C → B be two functors and let C be some object of C. If these satisfy axioms of realizability categories, then C is equivalent to Asm(B, (A, ·), φ) for some partial applicative structure (A, ·) and some combinatory complete filter φ.
The axioms of realizability categories indeed determine if an embedding of a Heyting categories F : B → C is equivalent to ∇ : B → Asm(B, (A, ·), φ) for some partial applicative structure (A, ·) and some combinatory complete external filter φ. In that sense the axiomatization is complete. 4.4. Slices. As conclusion to this paper, I show one application of the axioms of realizability: the proof that slices of categories of assemblies are realizability categories.
Definition 50. For each assembly I in Asm(B, (A, ·), φ) let B/I be the category of prone maps into I. Let A/I be the projection ∇A × I → I and let (A/I, ·) the constant partial applicative structure. Finally, for each U ⊆ ∇A × I let π 1 : U → I be in φ/I if the projection is a regular epimorphism. Proof. The category B/I is a reflective subcategory of Asm(B, (A, ·), φ)/I. The reflector sends x : X → I to the pullback T x of ∇Ux along η I : I → ∇UI and since both reindexing along η I and ∇U are regular functors, so is T . The unit θ x of the reflector is the factorization of η X : X → ∇UX through the projection T X = ∇UX × ∇UI I → ∇UX, which is a monomorphism, because it is the pullback of the monomorphism η I and equal to η T X . Hence θ x is a monomorphism and the reflector T is faithful. By naturalness of θ, ∇Ug 0 = ∇Up • h ′ . Since p is prone relative to ∇U there is a unique k : Z → Y such that ∇Uk = h ′ and p • k = g 0 . Because ∇Uθ is a natural isomorphism, ∇UT k = ∇Uh and T k = h by faithfulness of ∇U. By assumption T g = T (p, e • x) • h and T g 1 = T (e • x) • h = T (e • x • k) because T preserves limits. The functor T is faithful, so g 1 = e • x • k. Hence g = (p, x • e) • k. By generalization (p, x• e) is prone relative to T meaning there is a prone-regularlyepic span for each object in Asm(B, (A, ·), φ)/I.
The stability of the tracking axiom follows from the stability of the kinds of arrows involved. A morphism p : P → C × I is prone in Asm(B, (A, ·), φ)/I if it is the pullback of T p : T P → F U C × I along η C × I : C × I → F U C × I by lemma 36. Because the projection π 0 : C × I → C is the pullback of the projection π 0 : F U C × I → F U C along η C : C → F U C, the composition π 0 • p : T P → C is prone in Asm(B, (A, ·), φ).
Let f = (f 0 , f 1 ) : Y → (C × I) × I X be a monomorphism such that f 1 : Y → X is a regular epimorphism. Of course (C × I) × I X ≃ C × X, as C × I stands for a constant object of the slice. Any morphism P → X factors though f 1 because of the tracking axiom in Asm(B, (A, ·), φ) and this factorization works in the slice Asm(B, (A, ·), φ)/I because C × I is a constant object. The conclusion is that Asm (B, (A, ·), φ)/I is a realizability category and that it is isomorphic to Asm(B/I, (A/I, ·), φ/I) in particular.
The conclusion of this paper generalizes the lemma proved above.
Theorem 52. Slices of categories of assemblies are categories of assemblies.