Scott, Dana S. "Relating Theories of the Lambda-Calculus." (1980)

Section 1. Theories of Functions. The lambda-calculus is a theory of functions. We can relate this theory to other theories of functions.

First, in set theory we have a notion of functions from a set A to another set B, but since sets are extremely small compared to the class V of all sets, this tells us little about operations F:V->V on all sets. For example, union is an operator VxV->V, and in fact union can be applied to classes A and B to give a class A union B. Even though classes A and B are not in the domain of union, there is an obvious connection between the class operator union and the class A union B. We might consider forming a theory of class operations by passing to "hyperclasses." Another solution (Plotkin [1972]) is to only consider "continuous" class functions. These are class functions for which F(X) is a subset of F(Y) whenever X is a subset of Y and if A is a set with A subset of F(X), then there is some set B subset of X with A subset of F(B). These class functions can be described by the class {(a,B) | a,B sets with a in F(B)}. With this restriction, there is no need to pass beyond the level of classes. This operator theory (of continuous class functions) gives a model of lambda-calculus.

General category theory provides a much purer theory of functions than set theory. Category theory gives a theory of functions under composition and is also a theory of types. Category theory is extensional in the sense that functions (arrows) defined in different ways may be identical and that identical functions (arrows) can always replace one another. Some intensional theories of functions do not provide categories.

The axioms of category theory do not imply the existence of anything (there is an empty category)--it has no "existential import" and was not meant to. Set theory on the other had has "too much existential import" and was meant to. We would like a "middle way": cartesian closed categories.

Section 2. A Theory of Types. CCC's provide a way of making new types from old. For example, we can form products of types and consider arrows f:A^n->B as n-ary functions. Products are described in the usual categorial way with projections p and q. (Also, we have terminal objects 1 with unique arrows 0_C:C->1.) We note that arrows from C into AxB correspond precisely to pairs of arrows from C into A and B. We do not have such a correspondence for arrows from AxB: Consider groups A and B and homomorphisms f,g:A->B. We might try to form h:A^2->B by h(<u,v>)=f(u)g(v), but this is not a homomorphism unless B is abelian.

Since we are interested in a theory of functions, we would like to be able to write equations giving relations between arbitrary functions. We can accomplish this using exponent types (A->B). Exponents are described in the usual categorial way, with evaluation arrows epsilon(BC):(B->C)xB->C and transpose operator Lambda(ABC)h:A->(B->C) on arrows h:AxB->C. We can also describe exponents in terms of functors (exponents are right adjoint to products: -xA -| -^A).

So, each CCC represents a theory of functions, and the theory of CCC's provides a theory of types. We might also consider "bigger" theories by assuming coproducts, infinite products, or a subobject classifier. Topos theory is an obvious example of such a "bigger" theory of types. In some sense CCC's are the appropriate theory, since Lambek has shown "there is a perfect correspondence between CCC's and (extensional) typed lambda-calculi." This correspondence is given by interpreting lambda-terms (in context) as arrows A0 x ... x A(n-1) -> B where B corresponds to the type of the term and the Ai's correspond to the types of the free variables. Application is interpreted by composing with the evaluation arrow. Lambda abstraction is interpreted by taking the transpose (possibly after rearranging the context). The equations corresponding to the universal mapping property of exponents (epsilon o <(Lambda h) o p,q> = h and Lambda(epsilon o <kop,q>)=k) correspond to beta- and eta-reduction, respectively.

Given a particular CCC, the theory of functions it represents has types given by the objects, logical constants given by o, 0(used for !:C->1), p, q, <.,.>, epsilon, and Lambda, and nonlogical constants given by f:A->B. Equations f=g are the assertions of the theory. Some equations are logical axioms--those which hold in all CCC's. The other equations are those which happen to hold in the particular CCC. Note that these equations contain no variables. This corresponds to the fact that in lambda-calculus we can replace an equation M=N by the equivalent closed equation lambda x-bar M = lambda x-bar N where x-bar includes FV(MN). In the category this closure corresponds to a "heavy use of Lambda".

The correspondence is made complete by noting we can start with a (typed) lambda-theory and form a (syntactic) CCC representing the same theory of functions. The objects are the types (closed under 1, products, and exponents) and arrows are given by equivalence classes of terms "lambda x tau":A->B.

We may consider the typed lambda-calculus as a notational device for giving the functional equations describing a CCC. That is, starting from a primitive notion of maps under composition, we close the types under 1, products, and exponents. The lambda-calculus gives us a way of giving the functional equations. Since the Yoneda embedding allows us to embed any (small) category C into the CCC Set^{C^op} [actually, this is a topos], we see that this closure does not give us any new equations--so it is conservative [hence, consistent] to close the types under 1, products, and exponents.

Each CCC can be considered a theory (as opposed to a model). A CCC provides a model if it is concrete [well-pointed] --defined here to mean that we have enough elements a:1->A to distinguish between any distinct arrows f,g:A->B (for all A). Note that this condition allows us to recast the category in terms of sets and functions (the sets as objects are Hom(1,A) and the functions as arrows are given by f(x)=fox where f:A->B and x is in Hom(1,A)--we may also show that the products are really Cartesian products and exponents are really function spaces [usually not the full Set function space!] by associating arrows with their names). For an arbitrary CCC, Lambek showed how to adjoin infinitely many indeterminates x:1->A for each domain A and make the expanded category concrete--thus providing a model. Compare this to forming free algebras of equational theories.

We may think of the arrows in the CCC C (the "theory") as the definable maps. So, the idea is that we may need to expand the collection of elements in order to obtain a model.

Section 3. "Type-Free" Domains. The untyped lambda-calculus (without eta) can be considered as a special case of the typed lambda-calculus in the following sense. We find a domain U in a concrete CCC so that (U->U) is a retraction of U, i.e., there are maps i:(U->U)->U and j:U->(U->U) so that ji=1. Note that i is injective (so we may think of (U->U) is a subspace of U) and j is surjective (so we may think of (U->U) as a quotient space of U)--and the injection and surjection are related. We can interpret the untyped lambda-terms by converting them to typed lambda-terms interpreted in the category as follows: x*=x:U, (MN)* = j(M*)(N*), (lambda x.M)*=i(lambda x.M*). Note each M* is of type U. M=N in the type-free theory iff M*=N* in the category. Since we are assuming the CCC is concrete, U has "enough points" so that we have Rule zeta satisfied (giving weak extensionality--hence, a lambda-model). [Extensionality--the eta-rule--corresponds to the condition ij=1 giving U isomorphic to (U->U).]

Also, given a type-free theory, there is a CCC with a domain U with retract (U->U) so that the above interpretation satisfies precisely the same equations as the theory. This category is formed by taking the Karoubi envelope as in Barendregt. [There is a slight difference in the definition of products and projections.] The U is given by the identity lambda-term and the i and j are given by the lambda term 1=lambda fx.(fx) and (U->U) is also 1. Actually, every object A is a retract of U by arrows A:A->U and A:U->A. Given these definitions, it is easy to check that the interpretation of an untyped lambda term is the term itself.

Type-free domains are special kinds of types. In particular, to find a nontrivial U (i.e., U not a singleton), we must pass to an infinite type. This is already suggested in the construction of D-infinity since each D{n+1} = (Dn->Dn) is obviously a higher type than Dn, so that the limit D-infinity is an infinite type.

Not all CCC's lead to a nontrivial interpretation of the type-free lambda-calculus. For example, in Set we cannot have (U->U) a retract of U (unless U is a singleton) by Cantor's Theorem. Since all CCC's provide an interpretation of the typed lambda-calculus, we may consider the typed theory to be more general and more fundamental.

When considering models of lambda-calculus, we need Rule zeta to be satisfied. For this we need "enough elements." A solution to this problem is to adjoin indeterminates. For example, the open term model is a lambda-model (Rule zeta is satisfied) but the closed term model may not be a lambda-model (it is only a lambda-algebra if it does not satisfy Rule zeta). This description of [weak] extensionality in terms of having "enough" elements is unsatisfactory. However, we can axiomatize what a model must satisfy in order to be a lambda-model. First, note that we interpret lambda-terms by converting to terms in combinatory logic (removing the unalgebraic lambda-bindings). An applicative structure with elements S and K is a lambda-model if it satisfies:

1. The axioms for S and K: Kxy=x and Sxyz=xz(yz).

2. The [Meyer-Scott] axiom: forall x fx=gx implies BIf = BIg where I=SKK and B=S(KS)K. Note that BIfx reduces to fx, so that BI plays the role of 1. Similarly, B^nI plays the role of 1_n.

3. The axioms S=B^3IS and K=B^2IK which ensure that S and K are the canonical representatives of the 3-ary and 2-ary functions they represent.

Note that 1_n may be considered a retraction of U onto (U->(U->...->U...)).

Section 4. A Role for Intuitionistic Logic. Lambda-theories are equational, and we can expand the equational theory to a first-order theory without any new equations being forced on us. The axiomatization of the untyped lambda-calculus by S, K, Meyer-Scott and 1_3 S=S and 1_2 K=K gives the corresponding first-order theory. In the typed case, we get a many-sorted first-order theory. However, we would like to expand lambda-theories conservatively to higher-order theories in which we can (in some sense) talk about "all" functions. For the untyped lambda-calculus, this is impossible using a classical higher-order theory (with full comprehension) since we can prove Cantor's Theorem (so there can be no surjection j:U->(U->U) unless U is a singleton). This is also impossible in the typed case, since there are many typed lambda-calculus theories in where there are types such as U. An alternative is to use higher-order intuitionistic logic.

The idea is that we can embed a (small) category C into the topos Set^{C^op} which gives a model for higher-order intuitionistic logic. Since the Yoneda functor is an embedding, we have that the extension is conservative.

Consider first the structure of Set^{C^op}. The objects are functors F:C^op->Set giving sets FA (for each object of C) and functions Ff:FA->FB (for each f:B->A) so that F1_A = 1_{FA} and F(fg)=Fg o Ff. The arrows are natural transformations nu:F->G giving arrows nu_A:FA->GA so that nu_B o Ff = Gf o nu_A for f:B->A. An example of such a functor is given by H_C = Hom(-,C):C^op->Set. [Think: Hom(Antecedent,Succedent) and we reverse arrows--negate?--when we move from one side to the other.] The Yoneda lemma shows that every natural transformation H_A->H_B is uniquely of the form H_g for g:A->B (i.e., Yoneda H:C->Set^{C^op} is full and faithful).

We can describe the objects of Set^{C^op}, following Lawvere, as "variable domains" given by UA (indexed by A) with a "restriction" operation |f:UA->UB for each arrow f:B->A. So, each a in UA "restricts" to a|f = Uf(a) in UB (f provides a "transition" of a to a|f). Note that U is a functor iff the corresponding restriction operation satisfies a|1=a and (a|f)|g = a|fg. [Also note that this is a way of handling the notation of contravariant functors so that composition appears to be preserved.] Natural transformations are families of maps nu_A:UA->VA which commute with restriction, so that nu_B(a|f) = (nu_A(a))|f for all a in UA and f:B->A.

The terminal object is given by the domains {0} and restrictions 0|f = 0. Products can be formed by taking the products of the domains and the restrictions.

Exponents are more complicated. Given variable domains U and V, the exponent domains (U->V) are given by (U->V)A = {(phi_f)_f:UB->VB where f is indexed over f:B->A and the family satisfies phi_f(b)|g = phi_{fg}(b|g) [i.e., phi_{fg} o Ug = Vg o phi_f] for g:C->B and b in VB}. Restriction for f:B->A |g:(U->V)A->(U->V)B is given by (phi_h)_h|f = (phi_{fg})_g (the "future version" of (phi_h)_h after f has occurred). Note in particular we have phi_f o U1 = V1 o phi_1 for any phi in (U-V)A, f:B->A, and 1=1_A. This gives the functor U->V.

Epsilon:(V->W)xV->W is the natural transformation given by Epsilon_A:(V->W)A x VA -> WA with Epsilon_A((phi_f)_f,a) = phi_1(a). Epsilon is natural since (Epsilon_A(phi,a))|f = (phi_1(a))|f = phi_f(a|f) = (phi|f)_1(a|f) = Epsilon_B(phi|f,a|f).

Given psi:UxV->W, we form Lam(psi):U->(V->W) as the natural transformation Lam(psi)_A:UA->(V->W)A so that Lam(psi)_A(a) = (lambda b psi_B(a|f,b))_{f:B->A}. Lam(psi)_A does map into (V->W)A since it gives an indexed family of functions so that for f:B->A, g:C->B, a in UA, and b in VB, we have ((Lam(psi)_A(a))_f(b))|g = (psi_B(a|f,b))|g = psi_C(a|fg,b|g) = (Lam(psi)_A(a))_{fg}(b|g). Lam(psi) is natural since for a in UA, c in VC, f:B->A and g:C->B we have (Lam(psi)_A(a)|f)_g(c) = (Lam(psi)_A(a))_{fg}(c) = psi_C(a|fg,c) = psi_C((a|f)|g,c) = (Lam(psi)_B(a|f))_g(c).

The universal mapping property of exponents follows from the equations (where psi:UxV->W, k:U->(V->W), u in UA, v in VA, f:B->A, b in VB):

Epsilon o (Lam(psi) x 1) = psi since Epsilon_A(Lam(psi)_A(u),v) = (Lam(psi)_A(u))_1(v) = psi_A(u|1,v) = psi_A(u,v).

Lam(Epsilon o (k x 1)) = k since (Lam(Epsilon o (k x 1))_A(u))_f(b) = (Epsilon o (k x 1))_B(u|f,b) = Epsilon_B(k_B(u|f),b)) = (k_B(u|f))_1(b) = (k_A(u))_f(b).

Power objects in Set^{C^op} are given by PU where (PU)_A={{(S_f)_f{f:B->A}| S_f subset of U_B and b in S_f implies b|g in S_{fg} whenever g:C->B}. Restriction is given by (S|f)_g = S_{fg}.

A categorial element alpha:1->U gives an element a_A = alpha_A(0) in each UA so that a_A|f = a_B for all f:B->A. (Note, in particular, that for different f,f':B->A [different paths through time] we must have a_A|f = a_B = a_A|f'.)

If the category C is a CCC, then the Yoneda embedding maps C into a subcartesian closed category of Set^{C^op}. Clearly, H maps any terminal 1 to a terminal H_1 = Hom(-,1). It is easy to show that H_(AxB) is naturally isomorphic to H_A x H_B. We can also show that H_(A->B) is naturally isomorphic to (H_A -> H_B). To show this we must give a member of H_(A->B) (i.e., arrow C->(A->B)) for each phi in (H_A -> H_B), give a member of (H_A -> H_B) for each t in H_(A->B) (i.e., each t:C->(A->B)), and show that these constructions are natural and are inverses. Note that "restriction" in H_A is given by f|g = fog for f:B->A and g:C->B.

For phi in (H_A -> H_B) we have Lam(phi_p(q)):C->(A->B) where p:CxA->C and q:CxA->A are the obvious projections. For t:C->(A->B) we have tau in (H_A -> H_B) by tau_f(g) = epsilon o <t o f,g> for each f:D->C and g:D->A. This tau is really a member of (H_A -> H_B) since for f:D->C, g:D->A, and h:E->D, we have tau_f(g)|h = epsilon o <t o f,g> o h = epsilon o <tfh,gh> = tau_{fh}(gh) = tau_{fh}(g|h).

These operations form natural transformations. Starting with phi in (H_A -> H_B) we can show Lam((phi|h)_{p'}(q')) = Lam(phi_p(q))|h by taking the transpose of Lam(phi_p(q))|h = Lam(phi_p(q)) o h to obtain epsilon o ((Lam(phi_p(q)) o h) x 1) = epsilon o (Lam(phi_p(q)) x 1) o (h x 1) = phi_p(q) o <hp',q'> = phi_p(q)|<hp',q'> = phi_{hp'}(q') = (phi|h)_{p'}(q') which is the (unique) transpose of Lam((phi|h)_{p'}(q')). Starting with t:C->(A->B), we have tau^t|h = tau^{t|h} since (tau^t|h)_f(g) = tau^t_{hf}(g) = epsilon o <thf,g> = tau^{th}_f(g).

These operations are mutually inverse. If tau is obtained from Lam(phi_p(q)), then tau_f(g) = epsilon o <Lam(phi_p(q)) o f,g> = epsilon o (Lam(phi_p(q)) x 1) o <f,g> = phi_p(q) o <f,g> = phi_p(q)|<f,g> = phi_{p<f,g>}(q<f,g>) = phi_f(g). Conversely, epsilon o (Lam(tau_p(q)) x 1) = tau_p(q) = epsilon o (t x 1) implies Lam(tau_p(q)) = t.

So, we can embed a category C into the topos Set^{C^op}. We can use this embedding to conservatively extend the equational theory of C to a full intuitionistic higher-order theory. The interpretation of higher-order logic in Set^{C^op} looks like Kripke semantics, except that the "times" (as Lawvere has emphasized) form a category instead of a poset. We start with the objects of C as type symbols. We then expand the set of type symbols to be freely closed under products, exponents, and power types. Note that if C has product objects and exponent objects already, then the new product types and exponent types will be different, but will be isomorphic (in the appropriate sense). Thus, we can extend the notation H_T(A) to include all types T by taking product types to be the products in the functor category, exponent types to be the exponents in the functor category, and similarly with power types.

The logical language will have infinitely many variables of each type. The atomic formulae of the logical language will consist of false, x=y (where x and y are of the same type), y=fx where f:A->B in C (treated logically as a constant symbol) and x is type A and y is type B, z=(x,y), z=x(y), and 'y in x' where everything is assumed to be appropriately typed. Compound formulae are generated as usual. We can define a forcing-satisfaction relation A||-phi[s] where A is an object in C, phi is a formula, and s maps variables of type T to H_T(A). The definition begins by interpreting the atomic formulae in the obvious way and inductively extends the definition to compound formulae. The nontrivial cases are implication and universal quantification. For implication, we have A||-[phi -> psi][s] iff forall f:B->A B||-phi[s|f] implies B||-psi[s|f]. For universal quantifiers, we have A||-forall x.phi[s] iff forall f:B->A and b in H_T(B) B||-psi[s|f(b/x)]. The notation s|f obviously means the valuation given by s(x)|f for each x. (We may think of B as being "later" than A via the passage of time given by f.)

Keep in mind that H_T(A) may be empty.

We have the "functorial" character [or, persistence property] of ||-: if A||-phi[s] and f:B->A, then B||-phi[s|f]. This can be used to show that set comprehension holds. The appropriate "set" (map into the power object) for the formula phi(y) where y is of type T (with parameters given by s) is given by c_f = {t in H_T(B) | B||-phi[s|f(t/y)]}. It is easy to see that this is precisely the c we want. To show that c is actually in P(H_T), we need to show forall f:B->A, g:C->B, and b in c_f, we have b|g in c_{fg}. This follows since B||-phi[s|f(b/y)] implies C||-phi[s|(fg)(b|g/y) by the functoriality of ||-. We can also verify functional comprehension by defining a member of (H_T -> H_S) in a similar way. We can also verify that both set and functional extensionality are forced.

We can use the fact that the Yoneda embedding is faithful to show that for f,g:A->B in C "forall x,y [y=fx iff y=gx]" is valid (i.e., forced at all A) iff f=g. Also, h=gf implies "forall x,y,z [[y=fx and z=gy] -> z=hx]". We can also check identity axioms. Since we may have empty domains, it is a nontrivial fact that f:A->B is "well-defined" in the sense there "forall x exists y y=fx" is valid. Also, if A and B are objects of C ("ground types") and "forall x exists y forall z [z=y iff phi]" is valid, then there is an arrow f:A->B in C so that "forall x,z [z=fx iff phi]" is valid. So, we do have a conservative extension of the equational theory of C (we have an "exact picture of C at the level of ground types").

Since the Yoneda embedding preserves the CCC structure of C (if C is a CCC), then we find that we can conservatively extend a typed lambda-theory to be an intuitionistic higher-order theory. Said another way, the exponent types in C are interpreted (via Yoneda) as exponent types (the type of "all functions") in Set^{C^op}. So, the principles of lambda-calculus are consequences of intuitionistic higher-order logic [i.e., all our models satisfy the principles of lambda-calculus]. Scott concludes: "This seems to me to establish complete harmony between (intuitionistic) logic and (typed) lambda-calculus."

We can look for other ways to conservatively extend the equational theory of C by embedding C into other topoi which correspond to other logics (for example, the category of sheaves corresponds to including a modal operator in the logic).

Section 5. Type-Free Domains Revisited. In intuitionistic logic, we may have types U with the type (U->U) as a retract. In fact, we may embed any lambda-theory (any CCC) into a higher-order logic with such a U. The idea of the construction is as follows. Suppose we have some types A, B, and C that we are interested in (possibly multivariate) functions between. We can embed these types and maps into the category of "injective" spaces. For simplicity, assume A, B, and C are given by sets and we have them and the functions of interest in some (small) category.

An "injective" space is a T0 topological space D (points are determined by their neighborhoods) so that every continuous f:X->D with X dense in Y extends to f-:Y->D. The category of "injective" spaces is given by such D and continuous functions between them.

A set A can be made into an injective space A* by lettings A*={empty}union{{a} | a in A}. The topology on A* has basis {{a}} [so that every point is isolated except empty--and the only neighborhood of empty is the whole space]. It is easy to show this A* is "injective" (extend f:X->A* to f-:Y->A* by taking f-(y)={a} if there is a neighborhood N of y so that f is constantly {a} on N intersect X; otherwise let f-(y)=empty). Note that A is a dense subspace of A*. So, every g:A->B can be completed to give g*:A*->B*. We must have g*({a})={g(a)} so that if g*=h*, then g=h. This gives us a faithful functor * from the category containing A, B, and C into the injective spaces.

In the category of injective spaces, we can solve the domain equation U=A* x B* x C* x (U->U) giving an injective space U with retracts A*, B*, C*, and (U->U). (This idea can be realized for any set of injective spaces, not just for a finite number of special spaces such as A*, B* and C*.) Let C be the category of retracts of U. We may consider C to be small. Note that C includes A*, B*, and C*. We can embed C into the topos (or, higher-order theory given by) Set^{C^op}.

We have a full and faithful picture of our original sets and functions in Set^{C^op}. Let K_A be the variable domain given by K_A(V) = {f:V->A* | f is constantly {a} for some a in A}. Restriction on K_A is given by precomposition (a restriction of the restriction given by H_{A*}) so that f:W->V gives |f:K_A(V)->K_A(W). So, K_A is a subfunctor of H_{A*}. Natural transformations nu:K_A->K_B correspond precisely to maps |nu|:A->B. So, K is a full and faithful functor from our original category into Set^{C^op}.

The conclusion is that we can embed our original (typed) theory of functions into a theory containing a model of the type-free lambda-calculus given by a reflexive U. Furthermore, we can consider our original types A to be subtypes of U. Since (U->U) is a retract of U, every function f:A->B is the restriction of a function in (U->U). This is only necessarily true for the types A, B and C given in advance--not for all subtypes of U.

Engeler [1979] showed that lambda-models can incorporate any algebra (set with a binary operation). We can prove this result here. Given an algebra *:AxA->A, form the partial algebra *:A*xA*->A* and take the lambda-calculus model given by U where U=A*x(U->U). Every x in U may be regarded as a pair (x0,x1) where application f(x) is given by f1(x). Using the fixed point theorem (of the untyped lambda-calculus), there is a continuous rho satisfying rho(a)=(a,lambda x:U rho(a*x0)). This rho is clearly one-to-one. rho(a)(rho(b)) = rho(a*(rho(b))0) = rho(a*b). So, rho takes the partial algebra on A* injectively into U (with the application operation).

We might suspect that this result allows us to embed nonextensional combinatory algebras (in an application preserving way) into an extensional model. However, we do not have preservation of S and K. If we perform the construction above, we do know that application is preserved, but we only know that S and K operate as S and K on the subalgebra corresponding to the image of A*, not on all of U.

Section 6. Summary and Conclusions. The principal conclusions of the paper can be summarized in the following six points.

1. "A theory in typed lambda-calculus is just the same as a cartesian closed category."

This follows from the work of Lambek. Category theory is more general, however, since we do not assume the types are freely generated, just that they form an algebra under products and exponents.

2. "In a CCC a reflexive domain provides an interpretation of the 'type-free' theory."

3. "Every type-free theory is the theory of a reflexive domain in a CCC."

4. "Every CCC can be fully and faithfully embedded in an intuitionistic theory of types with the full (impredicative) power-set construct and function spaces (higher-order intuitionistic logic)."

This implies we can conservatively extend the equational theory of a CCC to an intuitionistic higher-order theory. This paper uses the topos Set^{C^op} (one of the first topoi of topos theory). By using other topoi, we may obtain different theories. Note also that this result implies that if we can prove the existence of a function f:A->B (where A and B are from our original category) in the intuitionistic higher-order theory, then this implies there really is an arrow f:A->B. That is, all such functions are lambda-definable.

5. "Every given CCC can be realized fully and faithfully as a category of subtypes of a reflexive type in a higher-order theory."

6. "Any (partial) algebra can be isomorphically represented as an applicative subalgebra of a reflexive domain."

We may ask how much stronger the intuitionistic higher-order theories can be made and still allow conservative extensions of given categories. The sentences satisfied by such theories correspond to internal properties of the topos we are using. For example, there are toposes in which Church's thesis (all number theoretic functions are recursive) is satisfied and Brouwer's Theorem (all real functions are continuous) is satisfied.