(1) A category C is said to be \underline{cartesian} iff it admits finite products — in other words, iff it has a terminal object, which we shall write 1 or ⊤, and every two objects A and B have a product which we write A × B or A ∧ B.

(2) A category C is said to be \underline{cartesian closed} iff it is cartesian and for every object A, the contravariant functor — × A which takes an object C to C × A (and a morphism f: C → C′ to (f, 1_{A}): C × A → C′ × A) has a right adjoint. This right adjoint will be written (—)^{A} or — ⇐ A or A ⇒ —. We call B^{A} the \underline{internal hom} of A and B, or the \underline{exponential} of B by A. It is characterized by the fact that every morphism C × A → B determines uniquely and naturally a morphism C → B^{A}. We also write this

\frac{C ∧ A ⊢ B}{C ⊢ A ⇒ B}

(when talking of proofs, we shall generally write ⊢ instead of →) and we call it the \underline{deduction theorem}.

(3) Anticipating on what follows, the objects in a cartesian closed category will also be called the \underline{types} of the category, or its \underline{statements}. An arrow f: X_{1} × ⋯ × X_{n} → A will be called a \underline{term} of type A with free variables of type X_{1}, …, X_{n}, or alternatively a \underline{proof} of A from the hypotheses X_{1}, …, X_{n}. When n = 0, this reduces to f: 1 → A, and we say that f is a global point of A, or a (closed) term of type B, or a proof of A (with no hypothesis). We note that it is always possible (by composing with the appropriate projection arrow) to add free variables to a term, and we shall not generally distinguish two terms that differ only by dummy free variables.

(4) The identity morphism B^{A} → B^{A} gives, under the functor adjunction, a morphism B^{A} × A → B (which is none other than the counit of the adjunction) which we call the \underline{evaluation map} ϵ, which we can also write (A ⇒ B)∧A ⊢ B. Thus, if g: X_{1}×⋯×X_{n} → B^{A} is a term of type B^{A} with free variables of types X_{1}, …, X_{n} and f: X_{1} × ⋯ × X_{n} → A is a term of type A with free variables of types X_{1}, …, X_{n}, we can form a term ϵ(g, f): X_{1} × ⋯ × X_{n} → B of type B with free variables of types X_{1}, …, X_{n}, called the composition of g and f (though the term “application” is probably better), and written g^{∫} f, or simply gf when no confusion can occur. We also make the convention that hgf will stand for (hg)f (which is in general distinct from h(gf)). To summarize, a term of type B^{A} and a term of type A can be composed to give a term of type B, provided they have the same free variables (which we can always assume). We write this

\frac{Γ ⊢ A ⇒ B , Γ ⊢ A}{Γ ⊢ B}

and we call it the \underline{rule of modus ponens}.

(5) On the other hand, if we have f: X_{1}×X_{n} → B a term of type B with free variables of types X_{1}, …, X_{n}, and A = X_{i} is one of these types, we can use the deduction theorem to form a new term of type B^{A} with free variables of types X_{1}, …, X̂_{i}, …, X_{n}: we shall write it λ[x_{i} : X_{i}].f, and we say that it is obtained from f by \underline{abstraction} of the i-th free variable. Note that in the process of writing f we shall write x_{i} for the identity on X_{i} so that we know what variable we are abstracting.

(6) To take a few examples, if A is a type, we have a term I_{A} = λ[x : A].x of type A ⇒ A, which we shall (somewhat abusively, of course) call the identity on A (in fact, it is an arrow from ⊤ to A^{A}, but there is no harm in seeing it also as an arrow from A to A). If A and B are types, we have a term K_{A,B} = λ[x : A].λ[y : B].x of type A ⇒ (B ⇒ A). And if A, B, C are types, we have a term

S_{A,B,C} = λ[x : A ⇒ (B ⇒ C)].λ[y : A ⇒ B].λ[z : A].xz(yz)

of type (A ⇒ (B ⇒ C)) ⇒ (A ⇒ B) ⇒ (A ⇒ C). When writing such terms we shall often refrain from explicitely writing the type of each variable in an abstraction, and leave it to the reader to calculate them. So we might simply write S_{A,B,C} = λx.λy.λz.xz(yz) which we abbreviate as S_{A,B,C} = λxyz.xz(yz).

(7) We note that every term which can be formed from the composition and abstraction operations can actually be formed by composition from its free variables and from the three terms I, K, S. Indeed, to do this we only have to show that we can eliminate one level of abstraction. But λx.x = I; and if f does not involve x then λx.f = Kf; and for composition we have λx.fg = S(λx.f)(λx.g), so that we can propagate the abstraction downwards until it hits either a variable x alone or a term that does not involve x. For example, we have

\begin{aligned}λx.λy.yx & = λx.S(λy.y)(λy.x) = λx.SI(Kx) \\ & = S(λx.SI)(λx.Kx) = S(K(SI))K \end{aligned}

(where we have used the fact that λx.Kx = K). In fact, I also can be eliminated since I = SKK. Of course, we shouldn’t be omiting the indices: if x has type A and y has type A ⇒ B, the expression above has type A ⇒ (A ⇒ B) ⇒ B and should be written

S_{A,(A⇒B)⇒A,(A⇒B)⇒B}(K_{((A⇒B)⇒A)⇒(A⇒B)⇒B,A}(S_{A⇒B,A,B}I_{A⇒B}))K_{A,A⇒B}

(8) We shall speak of the proofs K and S (of A ⇒ (B ⇒ A) and (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C respectively) as \underline{axioms}. In section (7) we have shown that every proof that can be obtained from the rule of modus ponens and the deduction theorem can actually be obtained with just modus ponens and the axioms K and S. In other words, we have “proven” the deduction theorem (provided one admits axioms K and S).

(9) There exists a unique term of type ⊤ with any kind of free variables: we shall write it ⋆, and we also call it an axiom. Similarily, for the ∧ operation, we have three rules of term creation: the two projections A ∧ B ⊢ A and A ∧ B ⊢ B, and the pair creation rule A, B ⊢ A ∧ B (this really means A ∧ B ⊢ A ∧ B, so it is really the identity map on A × B!). These rules allow us to create three important terms which we call axioms: p_{1,A,B} = λ[(x, y) : A ∧ B].x (of type A ∧ B ⇒ A), p_{2,A,B} = λ[(x, y) : A ∧ B].y (of type A ∧ B ⇒ B), and P_{A,B} = λ[x : A].λ[y : B].(x, y) (of type A ⇒ B ⇒ A ∧ B), with the obvious notations (namely that (x, y) means the term of type A × B that corresponds to the terms x and y of types A and B respectively by the universal property of A × B).

(10) A cartesian closed category is said to be \underline{bicartesian closed} iff it admits finite coproducts — in other words iff it has an initial object, which we shall write 0 or ⊥, and every two objects A and B have a coproduct which we write A + B or A ∨ B. In a bicartesian closed category, we also write ¬A for A ⇒ ⊥.

(11) A term x of type A defines a term of type A ∨ B which we shall write x^{←}, and similarily for a term of type B which defines a term x^{→} of type A ∨ B. These are two of the three rules for disjunction, namely the two canonical maps A ⊢ A ∨ B and B ⊢ A ∨ B. They give rise to two axioms q_{1} = λ[x : A].x^{←} which is a proof of A ⇒ A ∨ B, and q_{2} = λ[x : B].x^{→} which is a proof of B ⇒ A ∨ B. To define a term of type A ∨ B ⇒ C, things are a bit more complicated: by the universal property of A ∨ B (and one more of a great number of applications of the deduction theorem), such a term corresponds bijectively to a term of type A ⇒ C together with a term of type B ⇒ C. We say that we are defining a term by “discriminating cases”, and we shall write λ[x : A∨B].(f_{1}|f_{2}) where f_{1} is a term in which x appears free with type A and f_{2} is a term in which x appears free with type B. Except that to remove the ambiguity as to which variable we are discriminating for, we shall write x_{←} instead of x in the term f_{1} and x_{→} instead of x in the term f_{2}. This allows us to define another axiom, namely Q = λ[x : A ⇒ C].λ[y : B ⇒ C].λ[z : A ∨ B].(xz_{←}|yz_{→}), which has type (A ⇒ C) ⇒ (B ⇒ C) ⇒ A ∨ B ⇒ C. To illustrate some more the rules we propose for writing terms, we give the example of the term λ[x : A ∨ B].((x_{←})^{→}|(x_{→})^{←}): this term has type A ∨ B ⇒ B ∨ A and is precisely equal to Qq_{2}q_{1}.

(12) Finally, we should say something about ⊥. First of all, how to define a term of type ⊥: one just doesn’t. Second, how to define a term of type ⊥ ⇒ A: the universal property of ⊥ tells us that there is a unique proof ⊥ ⊢ A, and the deduction theorem then lets us manufacture a term of type ⊥ ⇒ A, which we write F = λ[x : ⊥].(), and this we call also an axiom.

(13) So let us recapitulate the axioms we have set up:

Name  Value  Type
K  λ[x : A].λ[y : B].x  A ⇒ B ⇒ A
S  λ[x:A⇒B⇒C].λ[y:A⇒B].λ[z:A].xz(yz)  (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
⋆  ⋆  ⊤
p_{1}  λ[(x, y) : A ∧ B].x  A ∧ B ⇒ A
p_{2}  λ[(x, y) : A ∧ B].y  A ∧ B ⇒ B
P  λ[x : A].λ[y : B].(x, y)  A ⇒ B ⇒ A ∧ B
F  λ[x : ⊥].()  ⊥ ⇒ A
q_{1}  λ[x : A].x^{←}  A ⇒ A ∨ B
q_{2}  λ[x : B].x^{→}  B ⇒ A ∨ B
Q  λ[x:A⇒C].λ[y:B⇒C].λ[z:A∨B].(xz_{←}|yz_{→}) (A ⇒ C) ⇒ (B ⇒ C) ⇒ A ∨ B ⇒ C

(14) These axioms have the interesting property, analogous to that which we saw in section (7) for only one connective, that every term that can be formed with the rules described can be actually written with just the axioms (and the free variables) using composition (that is, modus ponens) as the only rule. In particular, any closed term can be written with just the axioms. To give just one example, take the rule of de Morgan:

\begin{matrix}( & λ[(f, g) : (¬A) ∧ (¬B)].λ[x : A ∨ B].(fx_{←}|gx_{→}), \\ λ[h : ¬(A ∨ B)].(λ[x : A].hx^{←}, λ[x : B].hx^{→})) \end{matrix}

of type

(((¬A) ∧ (¬B)) ⇒ (¬(A ∨ B))) ∧ ((¬(A ∨ B)) ⇒ ((¬A) ∧ (¬B)))

(where we recall that ¬A means A ⇒ ⊥): it can be written

P (S(S(KQ)p_{1})p_{2})(S(S(KP)(S(S(KS)K)(Kq_{1})))(S(S(KS)K)(Kq_{2})))

(Nobody said it was interesting.) Since we’re talking about de Morgan, there is another rule of de Morgan, namely

λ[h : (¬A) ∨ (¬B)].λ[(x, y) : A ∧ B].(h_{←}x|h_{→}y)

of type

((¬A) ∨ (¬B)) ⇒ (¬(A ∧ B))

which can be written

Q(S(S(KS)K)(Kp_{1}))(S(S(KS)K)(Kp_{2}))

But that is all: there is no mysterious fourth rule, nothing like (¬(A ∧ B)) ⇒ ((¬A) ∨ (¬B))...

(15) A bicartesian closed category is said to be \underline{boolean} iff the natural morphism A ⊢ ¬¬A (obtained from the term λ[x : A].λ[h : ¬A].hx of type A ⇒ ¬¬A by the deduction theorem) is actually a (natural) isomorphism. In that case, we have a term W of type ¬¬A ⇒ A, which we call an axiom. For example, we can compose it with the term

λ[h : ¬(A ∨ ¬A)].h(λ[x : A].hx^{←})^{→} = SI(S(Kq_{2})(S(S(KS)K)(Kq_{1})))

of type ¬¬(A ∨ ¬A) to obtain a proof W (SI(S(Kq_{2})(S(S(KS)K)(Kq_{1})))) of A ∨ ¬A, the so-called tertium non datur. We can also form the term

λ[h : (A ⇒ B) ⇒ A].W λ[k : ¬A].k(hλ[ℓ : A].F (kℓ))

of type ((A ⇒ B) ⇒ A) ⇒ A, called “Pierce’s law”.

(16) We recall that any partially ordered set (poset) P can be made into a category by decreeing that there is exactly one morphism p → q whenever p ≤ q, and none otherwise. Now if we translate the conditions for P to be a bicartesian closed category in terms of the order structure, we find the following: P is a lattice with a least element ⊥ and a greatest element ⊤, and for any two elements p, q of P, the set of elements r such that r ∧ p ≤ q has a greatest element, written p ⇒ q: we have r ≤ (p ⇒ q) iff z ∧ p ≤ q. Such a poset we call a \underline{Heyting algebra}. Since — ∧ p is a left adjoint, it preserves coproducts, so we have (q ∨ r) ∧ p = (q ∧ p) ∨ (r ∧ p) (really, isomorphic, but isomorphic objects in a poset are equal), and the underlying lattice to a Heyting algebra is therefore distributive. In a Heyting algebra, we let (according to the general definitions given earlier) ¬p stand for p ⇒ ⊥: in other words, ¬p is the greatest of those elements q such that p ∧ q = ⊥. We then have p∧¬p = ⊥, but it does not follow that p∨¬p = ⊤, only that no q with p∧q = ⊥ will make p ∨ q any bigger. Any boolean algebra, of course, is a Heyting algebra (with p ⇒ q = q ∨ ¬p), but the converse is not true: the lattice of open sets on any topological space (or indeed of any locale) is a Heyting algebra, and it is a boolean algebra iff the space is a direct sum of indiscrete spaces. Actually, a Heyting algebra is boolean iff it is boolean as a bicartesian closed category (as defined in (15)).

(17) We now proceed to introduce quantifiers in our system. Before we do so, we digress a little from the path of pure rigour and explain something of what we are trying to achieve. We are trying to define something like ∀(x : U).V_{x} and ∃(x : U).V_{x}, which should be terms, that is, objects of our category. In this construction, V_{x} should be a term which depends on the variable x, and we take respectively the product and the coproduct of the corresponding terms, in accordance with the philosophy that in intuitionist logic, a proof of ∀(x : U).V_{x} is a function that takes every x to a proof of V_{x} and a proof of ∃(x : U).V_{x} is obtained by giving an x together with a proof of V_{x}. However, things are not altogether clear, because it is not clear what U is, and even less what x is, or how we should describe an type that varies in function of a variable: if we start writing things like λ[x : U].V_{x}, this looks suspiciously like a term, so it should have a type. But on the other hand, if we have a proof v_{x}: ⊤ ⊢ V_{x} of V_{x} for every x (whatever that means!) we get a term λ[x : U].v_{x} of type ∀(x : U).V_{x}, and the relations between the objects λ[x : U].v_{x}, λ[x : U].V_{x} and ∀(x : U).V_{x} are hard to describe in the framework that we have been using so far. Note that here we are forced to introduce one more level: proofs reside on one level, their types (viz.the propositions they prove) on another, and these types seem themselves to be terms of some kind, since it is possible to use some operations like λ on them. Now, U must reside on the highest level, but there is some confusion of the levels because U is quite similar to the type Ũ defined as ∃(x : U).⊤. For example, if V does not depend on x, then ∃(x : U).V is none other than Ũ ∧ V, and similarily, ∀(x : U).V is none other than Ũ ⇒ V.

Now that we have described the difficulties, how do we solve them? I believe the key to the problem lies in the complex hierarchy we mentioned. For example, take the case of Peano arithmetic: we can quantify over the natural numbers. So we will have to introduce a type, N, for the natural numbers, together with a term O of type N (the number zero, which we write O so as not to confuse it with an initial object), and a successor function S of type N^{N}. Note that we use the non-logical (but not illogical!) notation here because it doesn’t make much sense to speak of S as a proof of the fact that N implies N. Equality, on the other hand, is a term of type Ω^{N×N}, where Ω is a certain type, the type of logical propositions. And the terms of that type are propositions in the way we have been discussing them so far. For example, x = x is a term of type Ω with a free variable x of type N, and it is itself a proposition, which has a term in it, the proof of the fact that x = x. So we have three levels where we previously had only two (types and terms): the types of “big category” like N or Ω or Ω^{N×N}, which do not express a statement; the terms of type Ω, or propositions, which are themselves types of some kind, and express logical statements in the way we saw up to now, and the terms of those types, which are proofs. The top level category does not have anything remarkable about it: it is a bicartesian closed category with at least two types, N and Ω. It is the type Ω which is magical: its terms (with any, fixed, kind of free variables) themselves form a bicartesian closed category. We then say that Ω is an internal bicartesian closed category (quite a mouthful!), or a bicartesian closed category object. It is this framework that will allow us to define quantifiers in a satisfactory fashion. And note that as an extra bonus we get propositions with free variables in Ω^{N} and similar types — in other words, we automatically get a higher order logic where quantification is not only on natural numbers but on sets of naturals.

(18) Let C be a bicartesian closed category. We say that an object Ω of C is endowed with the structure of an internal bicartesian closed category when for every object U of C the set Ω(U) := Hom(U, Ω) (of terms of type Ω with a free variable of type U) is endowed with the structure of a bicartesian closed category, and this, in a functorial way (which means that whenever U → U′ is a morphism, the map of sets obtained by composition, Ω(U′) → Ω(U), is a morphism of bicartesian closed categories, in other words it is a functor that preserves the operations ⇒, ⊤, ∧, ⊥ and ∨). Or, to say things differently, an internal bicartesian closed category is a functor to the category of bicartesian closed categories that is representable by an object Ω of C. (Note that we are not imposing that the arrows of the internal category be representable: only the objects.) When P and Q are terms of type Ω with free variables of types U_{1}, …, U_{n} (that is, morphisms U_{1} × ⋯ × U_{n} → Ω), we can then define P ⇒ Q which is another term of type Ω with the same free variables (note that we can always arrange, by adding dummy free variables, to be in that case). Similarily, we have P ∧ Q, P ∨ Q and ⊤ and ⊥ (the two last have any free variables you want: we shall carelessly identify all the terms ⊤: U_{1} × ⋯ × U_{n} → Ω). We also have proofs between these terms of type Ω: if P, Q: U → Ω are terms of type Ω with U free (we omit the detailed structure), we have the morphisms x: P ⊢ Q from P to Q within the category structure of Ω(U). We then speak of proofs of Q on the assumption that P, but we may also add U as an assumption (or free variable type), even though that is implicit since it is free in P itself. We have two kinds of composition: first, given propositions P, Q, R: U → Ω and proofs P ⊢ Q and Q ⊢ R, we may construct a proof P ⊢ R by composition within Ω(U); second, given propositions P, Q: U′ → Ω, a proof P ⊢ Q and a morphism f: U → U′ we may use the functoriality of our constructions to yield a proof P f ⊢ Qf (this operation we call variable substitution because it corresponds to changing the free variable of type U′ in P and Q to a free variable of type U by means of the morphism f). Abstraction (the λ operation) is also possible, both internally (inside the category Ω(U)) and externally (in the category C). For example, consider the morphism Ω → Ω defined by P ⇒ P where P is the free variable of type Ω (as a side note, this morphism is well defined essentially by the Yoneda lemma, which states that a morphism between representable functors is the same thing as a morphism between the objects that represent them). One can abstract it externally to a morphism 1 → Ω^{Ω} defined as λ[P : Ω].(P ⇒ P). On the other hand, one can consider the identity morphism (inside Ω(Ω)!) P ⊢ P, which by internal abstraction gives (λ[x : P].x): ⊤ ⊢ (P ⇒ P), with free variable P of type Ω. One might then want to perform abstraction of P in this term, but this is neither internal abstraction (one is abstracting away a variable in C) nor external abstraction (the abstracted term resides in the internal category). It is the mixed abstraction of which we shall talk in a second: let us just say that we will get λ[P : Ω].λ[x : P].x which is a proof of ∀(P : Ω).(P ⇒ P), the latter being a proposition (in Ω(1), i.e.with no free variables) of type Ω.

(19) (The Universal Property of ∀.) Suppose Q_{x}: U × V → Ω is a term of type Ω with free variables x of type U and others of type V. We then define ∀(x : U).Q_{x} to be the term of type Ω with free variable of type V (i.e.the morphism V → Ω) that satisifies the universal property that we are about to describe, if it exists. The universal property concerns ∀(x : U).Q_{x} together with its projection which is a morphism p_{y}: ∀(x : U).Q_{x} ⊢ Q_{y} (in the category Ω(U × V), where we have added a fictitious free variable of type U to ∀(x : U).Q_{x}). It states: for any term P: V → Ω and any proof u_{x}: P ⊢ Q_{x} (in the category Ω(U × V), where we have added a fictitious free variable of type U to P), there exists a unique proof λ[x : U].u_{x} of ∀(x : U).Q_{x} from the assumption P which composed with the projection p_{y} of Q_{y} from the assumption ∀(x : U).Q_{x} gives precisely the proof u_{y} we started from. (Note that in all this the index x or y on terms is just to help remember what has a free variable. But Q_{x} and Q_{y} are the same thing, just a morphism U × V → Ω.) In other words, ∀(x : U).Q_{x} is universal for those terms of type Ω with free variable of type V (the important thing is that there is no longer the free variable x of type U) “which prove Q_{y}”.

Now consider Q_{x} and P as above. If u: P ⊢ ∀(x : U).Q_{x} and f: W → U is a term of type U with free variable of type W, then we write uf for the proof P ⊢ Q_{f} (where Q_{f} stands for the term W × V → Ω obtained by composing Q: U × V → Ω with f) obtained by composing u with the projection p_{f}: ∀(x : U).Q_{x} ⊢ Q_{f}. While this may sound arcane, what we’re doing is just applying a proof that ∀(x : U).Q_{x} to a term f of type U to get a proof of Q_{f}, which is reasonable. Note that with this notation, the projection p_{y}: ∀(x : U).Q_{x} ⇒ Q_{y} is simply λ[h : ∀(x : U).Q_{x}].hy.

(The Universal Property of ∃.) The universal property of ∃ is similar. Suppose P_{x}: U × V → Ω is a term of type Ω with free variables x of type U and others of type V. Then ∃(x : U).P_{x} is of type Ω and has only a free variables of type V, comes with a proof q_{y}: P_{y} ⊢ ∃(x : U).P_{x} such that for any term Q of type Ω that has only a free variable of type V and any proof u_{x} of Q from P_{x}, there exists a unique proof (x?u_{x}) of Q from ∃(x : U).P_{x} (x is not free) which composed with the proof q_{y} of ∃(x : U).P_{x} from P_{y} gives precisely the proof u_{y} we started from.

If P_{x} is as above, and f: W → U is a term of type U with free variable of type W, and Q: V → Ω is a term of type Ω with free variable of type V, and u_{f}: Q ⊢ P_{f} is a proof of P_{f} from Q, then we write (f, u_{f}) for the composition of the proof q_{f} of ∃(x : U).P_{x} from P_{f} and the proof u_{f} of P_{f} from Q. Also, concerning the notation (x?u_{x}) we introduced above (which says something like “since there exists such an object, call it x”), we make the convention that when writing u_{x}, the variable of type ∃(x : U).P_{x} which is being assumed will be written with an extra subscript x, because it then appears of type P_{x} (if this sounds obscure, compare with a case construction like λ[x : A ∨ A].(x_{←}|x_{→}) (of type A ∨ A ⇒ A) in which, although x has type A ∨ A, it is used with type A in the parentheses, which we recall with the arrow subscript).

Note that the objects ∀(x : U).R_{x} and ∃(x : U).R_{x} satisfying the universal properties we have just given may or may not exist. When they exist for any type U and any term R_{x} of type Ω with free variable of type U, we say that Ω is a \underline{complete} internal bicartesian closed category (whew!). We now make this assumption.

(20) We now give a few examples to illustrate the notations. First of all, let us prove that if U and V are types then

∀(f : Ω^{U×V}).(∃(x : U).∀(y : V).fxy) ⇒ (∀(y : V).∃(x : U).fxy)

To this effect, we take f a free variable of type Ω^{U×V} and h an assumption that ∃(x : U).∀(y : V).fxy. Now if h_{x} is an assumption that ∀(y : V).fxy (where the free variables are x of type U and f of type Ω^{U×V}) then h_{x}y is a proof of fxy (where we have added one more free variable, y, of type V), so that (x, h_{x}y) is a proof of ∃(x : U).fxy and λ[y : V].(x, h_{x}y) is a proof of ∀(y : V).∃(x.U).fxy. Now this was based on the assumption h_{x} that ∀(y : V).fxy, and therefore (x?λ[y : V].(x, h_{x}y)) is a proof of the same based on the assumption h that ∃(x : U).∀(y : V).fxy. Therefore λh.(x?λ[y : V].(x, h_{x}y)) is a proof of the implication, and finally the proof we wanted is

λ[f : Ω^{U×V}].λ[h : ∃(x : U).∀(y : V).fxy].(x?λ[y : V].(x, h_{x}y))