Electronic Notes in Theoretical Computer Science 73 (2003)

URL: http://www.elsevier.nl/locate/entcs/volume73.html LastPage pages

Exponentiation of Scott formal topologies

Maria Emilia Maietti - Silvio Valentini ^{1}

Dipartimento di Matematica Pura ed Applicata Università di Padova via G. Belzoni n.7, I–35131 Padova, Italy

Abstract We prove that Scott formal topologies are exponentiable in the category of inductively generated formal topologies. From an impredicative point of view, this means that Scott domains are exponentiable in the category of open locales.

1 Introduction

Formal topology is nowadays recognized as one of the main approaches to the development of constructive topology, where by constructive we mean intuitionistic and predicative.^{2}

Many results of classical and impredicative topology have been already studied predicatively by using formal topology (see [Sam03] for an updated overview on formal topology).

In formal topology one describes a topological space by building the frame of its open sets, starting from a set of basic open sets. While the problem of expressing the union of basic opens is easily solved by considering the set of the involved basic opens, to describe the intersection of two open sets two approaches are possible. In the first approach one defines formal topologies starting from a pre-ordered base and then he describes the intersection on subsets by means of the preorder; in the second approach one defines formal topologies starting from a base closed under a monoid operation which is lifted at the level of subsets. In both cases continuous relations can be introduced and then we can organize formal topologies into a category, that we call FTop_{↓} in the case of formal topologies based on a preorder and FTop_{•} in the case of formal topologies based on the monoid operation. Both FTop_{↓}

1 Email: maietti,silvio@math.unipd.it

2 Note that working in an intuitionistic and predicative setting means in particular that one is free to use the axiom of choice; indeed, on the contrary of what happens in an impredicative foundation like topos theory, it is constructively admissible.

\begin{matrix}c \\ ◯ \end{matrix}2003 Published by Elsevier Science B. V.

Maietti-Valentini

and FTop_{•} allow a predicative presentation of the category OpLoc of open locales [JT84,Joh84]. The two kinds of presentation remain impredicatively equivalent to OpLoc also when we restrict ourselves to consider their full subcategories of inductively generated formal topologies (see [CSSV03]), that is, FTop_{↓}^{i} and FTop_{•}^{i} respectively.

We can also consider formal topologies without the positivity predicate, called formal covers. They also can be organized into two categories, that we call FTop_{↓}^{−} and FTop_{•}^{−}, which are both impredicatively equivalent to the category Loc of locales [Joh82].

However, even if FTop_{↓} and FTop_{•} are equivalent categories, they differ when we consider unary topologies (see section 2.3). Indeed, whilst the full subcategory of the unary topologies of FTop_{↓} is essentially equivalent to the category of algebraic dcpos with bottom, the full subcategory of the unary topologies of FTop_{•}, called Scott formal topologies, is essentially equivalent to the one of Scott domains (see [SVV96]).

In this paper, instead of studying the category FTop_{•}, we restrict our attention to its subcategory FTop_{•}^{i}; indeed, this latter is predicatively known to be cartesian while FTop_{•} is not. Our main result is a proof that Scott formal topologies are exponentiable in FTop_{•}^{i}. From an impredicative point of view, our result states that Scott domains are exponentiable in OpLoc. An analogous result can also be proved, with similar proofs, for the more general case of unary topologies in FTop_{↓}^{i} (see [MV02]). However, it is worth studying the exponentiation of unary topologies in FTop_{•}^{i} because the subcategory of Scott formal topologies is predicatively cartesian closed (see [Val03]) while the one of unary formal topologies of FTop_{↓}^{i} is not.

It is worth noting that the proof of exponentiation of unary topologies that we propose here is intuitionistically valid even in an impredicative setting since in this case there is no need of using the axiom of choice. Checking this fact is almost straightforward everywhere in the proof apart for the point where we make use of co-induction to define the positivity predicate for the exponential topology. Indeed, whilst impredicatively the co-inductive definition we use can be easily justified by using Tarski fixed-point theorem, predicatively the justification of its existence requires much more care and it can be obtained according to the work by P. Martin-Löf’s, T. Coquand and E. Palmgren (see [Coq96,Pal02]).

As a consequence of our result, one also gets an entirely predicative proof that unary formal topologies are exponentiable in FTop_{•}^{i−}.

In the end of this introduction it can be useful to recall that the question of characterizing exponentiable topologies has a long history in the development of topology. Regarding classical topology, it is well known that the category Top of topological spaces and continuous functions is not cartesian closed. In fact, the topological spaces that can be exponentiated in Top are only those whose frames of open sets are locally compact locales (for an overview on this topic see [EHar]). This result was reproduced by Hyland in the context of the intuitionistic but impredicative theory of locales by showing that in Loc only the locally compact locales can be exponentiated [Hyl81]. Later, his proof of exponentiation was adapted to the language of formal topology, but still working within an impredicative setting (see [Sig95]). More recently, Vickers reproduced most of Hyland’s results by using geometric reasoning (see [Vic01]).

We think that our main contribution in proving exponentiation of unary topologies in FTop_{•}^{i} is a detailed analysis of the conditions characterising the continuous relations between a unary formal topology and an inductively generated one. In fact, after this analysis, the axioms to be used in order to define the cover relation of the exponential topology, and the corresponding positivity predicate, emerge naturally.

2 Formal topologies and their morphisms

In this section we recall the basic definitions of formal topology. The reader interested to have more details on formal topology and a deeper analysis of the foundational motivations for its development within Martin-Löf’s constructive type theory [Mar75,Mar98,NPS90] is invited to look for instance at [Sam03]. We start by recalling the definitions of •-formal cover and •-formal topology.

Definition 2.1 [Formal cover] A •-formal cover is a structure

A ≡ (A, ·, ⊤, ◁)

where A is a set, · is an associative binary operation between elements of A, ⊤ is a distinguished element of A and ◁ is an infinitary relation, called cover relation, between elements and subsets of A satisfying the following conditions:

(reflexivity) \frac{aεU}{a ◁ U} (top) a ◁ \{⊤\} (transitivity) \frac{a ◁ U U ◁ V}{a ◁ V}
(•-left) \frac{a ◁ U}{a · b ◁ U}  \frac{b ◁ U}{a · b ◁ U}  (•-right)  \frac{a ◁ U  a ◁ V}{a ◁ U · V}

where U ◁ V is a shorthand for (∀uεU) u ◁ V and U · V is a shorthand for the subset {u · v ∈ A | uεU & vεV }.

Definition 2.2 [Formal topology] A •-formal topology is a structure

A ≡ (A, ·, ⊤, ◁, Pos)

where (A, ·, ⊤, ◁) is a formal cover and Pos is a predicate over A, called the positivity predicate, satisfying the following conditions:

(monotonicity) \frac{Pos(a) a ◁ U}{(∃uεU) Pos(u)}
(positivity axiom)  a ◁ a^{+}

where a^{+} ≡ {x ∈ A | x = a & Pos(x)}.

It is interesting to note that if a cover relation admits a positivity predicate then such a positivity predicate is unique (see [MV02]).

Then, a formal point is defined as follows.

Definition 2.3 [Formal point] Let (A, ·, ⊤, ◁, Pos) be a •-formal topology. Then a subset α of A is a formal point if, for any a, b ∈ A and any U ⊆ A, it satisfies the following conditions:

(point inhabitance)  ⊤εα
(point directness) \frac{aεα bεα}{a · bεα}
(point splitness) \frac{aεα a ◁ U}{(∃uεU) uεα}

To explain the intended meaning of the cover relation and the positivity predicate, it is convenient to introduce the map ext(−) which associates to a basic open a ∈ A the collection of the formal points to which a belongs. Then, the intended meaning of the cover relation a ◁ U is that ext(a) ⊆ Ext(U), where Ext(U) ≡ ⋃_{uεU} ext(u) is the collection of points containing some element u of U, while the intended meaning of Pos(a) is that there exists a formal point in ext(a). It is trivial to check that, according to these meanings, the conditions on the cover relation and the positivity predicate in definition 2.2 are all valid.

Now, let us recall the notion of continuous relation between formal topologies. It expresses a predicative counterpart of the notion of locale morphism. The definition of continuous relation is obtained from the definition of frame morphism expressed in terms of relation in [Sam87] by taking the opposite relation.

Definition 2.4 [Continuous relation] Suppose A = (A, ·_{A}, ⊤_{A}, ◁_{A}, Pos_{A}) and B = (B, ·_{B}, ⊤_{B}, ◁_{B}, Pos_{B}) are two •-formal topologies. Then a continuous relation from A to B is a binary proposition aF b, for a ∈ A and b ∈ B, such that the following conditions are satisfied:

(function totality)  a F ⊤_{B}
(function convergence)  \frac{a F b a F d}{a F b · d}
(function saturation) \frac{a ◁_{A} W (∀wεW) w F b}{a F b}
(function continuity)  \frac{a F b b ◁_{B} V}{a ◁_{A} F^{−}(V)}

where F^{−}(V) ≡ {c ∈ A | (∃vεV) c F v}.

Some immediate consequences of the definition are the following.

Lemma 2.5 Let F be a continuous relation from A to B. Then, for any a ∈ A and b ∈ B, F satisfies the following conditions:

(function monotonicity) \frac{Pos_{A}(a)  aF b}{Pos_{B}(b)}
(function positivity)  \frac{Pos_{A}(a) → aF b}{aF b}

Note that function monotonicity was included in the original definition in [Sam87] but it was later observed to be derivable in [Neg02].

To organize formal topologies and continuous relations into a category we can not simply consider relation composition. Indeed, given any continuous relation F from A to B and any continuous relation G from B to C, G∘F is not a continuous relation because it satisfies all of the conditions for a continuous relation except for saturation. However, we can turn formal topologies and continuous relations into a category in the following way [Vir90].

Proposition 2.6 Formal topologies and continuous relations form a category FTop_{•} provided that, for any continuous relation F from A to B and any continuous relation G from B to C composition of relations is defined by setting, for a ∈ A and c ∈ C,

a G ∗ F c ≡ a ◁ {x ∈ A | (∃y ∈ B) x F y & y G c}

and the cover relation is used like unit.

Since the definition of continuous relation does not depend on the positivity predicate we obtain a category also in the case of considering formal covers as objects.

Definition 2.7 Formal covers and continuous relations form a category FTop_{•}^{−}.

The category FTop_{•} is impredicatively equivalent to the category OpLoc of open locales [JT84] (for a recent proof see [Neg02]) while FTop_{•}^{−} is impredicatively equivalent to the category Loc of locales (see [BS01]).

2.1 Inductively generated formal topologies

One of the main tools in formal topology is the inductive generation of the cover since this allows to develop proofs by induction. A general method for generating inductively formal topologies was proposed in [CSSV03]. It allows to construct the minimal cover relation which satisfies a given set of axioms. Here, we adapt this method to the framework of •-formal topology. Given a set of axioms, specified, for each basic open a ∈ A, by an axiom indexing set I_{A}(a) and, for each index i ∈ I_{A}(a), by a subset C_{A}(a, i) of A that is supposed to cover a, and a predicate Pos(−) satisfying

(axiom monotonicity) \frac{Pos(a) i ∈ I_{A}(a)}{(∃cεC_{A}(a, i)) Pos(c)}

and

(•-left monotonicity) \frac{Pos(a · b)}{Pos(a)} \frac{Pos(a · b)}{Pos(b)}

we can generate inductively a cover relation by using like inductive rules only reflexivity, •-left and the following new one:

(infinity) \frac{i ∈ I_{A}(a) C_{A}(a, i) ◁ U}{a ◁ U}

It is then possible to show that the cover so obtained respects the set of axioms I_{A}(−) and C_{A}(−, −) and the conditions top, reflexivity, transitivity, •- left and •-right, and also monotonicity and positivity with respect to the given positivity predicate, provided that in the axiom-set I_{A}(−) and C_{A}(−, −) that we are considering, there are indexes for the following subsets ^{3}

(localized top)  C_{A}(a, k_{1}) ≡ {a · ⊤}
(contraction)  C_{A}(a, k_{2}) ≡ {a · a}
(localized contraction) C_{A}(c · a, k_{3}) ≡ {c · a · a}
(exchange)  C_{A}(a · b, k_{4}) ≡ {b · a}
(localized exchange) C_{A}(c · a · b, k_{5}) ≡ {c · b · a}
(positivity)  C_{A}(a, k_{6}) ≡ a^{+}

and that it satisfies the following localization condition which guarantees the validity of •-right ^{4} .

Definition 2.8 [Localization condition] Let A be any set and I_{A}(−) and C_{A}(−, −) be an axiom-set for a cover relation on A. Then such an axiom-set satisfies the localization condition if, for any i ∈ I_{A}(b), there exists j ∈ I_{A}(a·b) such that C_{A}(a · b, j) ⊆ {a} · C_{A}(b, i).

Now, we are ready to introduce the following definition.

Definition 2.9 We call FTop_{•}^{i} the full sub-category of FTop_{•} whose objects are inductively generated formal topologies. Analogously, we call FTop_{•}^{i−} the

3 Not all requirements are necessarily needed. Indeed, in the presence of localized top, exchange and localized contraction then contraction is derivable, but we leave it to be modular. 4 This condition is a weaker variant of Johnstone’s meet stability condition on coverages [Joh82].

full sub-category of FTop_{•}^{−} whose objects are inductively generated formal covers.

From an impredicative point of view, FTop_{•}^{i} and FTop_{•} are equivalent likewise FTop_{•}^{i−} and FTop_{•}^{−}. On the other hand, from a predicative point of view, FTop_{•}^{i} and FTop_{•} are not equivalent because there are formal topologies which can not be generated by induction (see the last section of [CSSV03]).

It is interesting to observe that we can always turn an inductively generated formal cover into an inductively generated formal topology.

Proposition 2.10 (Coreflection) The category FTop_{•}^{i} is a coreflective subcategory of FTop_{•}^{i−}.

The proof of such a result in the context of formal topologies based on a preorder relation can be found in [MV03] and it can be easily reproduced in the context of •-formal topologies. The process of building the minimal inductively generated formal topology embedded into a given inductively generated formal cover is the following. Given any axiom-set I_{A}(−), C_{A}(−, −), one can show that it is always possible to define a predicate Pos(−) which satisfies both axiom monotonicity and •-left monotonicity by simply considering these conditions like co-inductive rules. Then, after the predicate Pos(−) has been defined, we can add to I_{A}(a) a new index ∗ and to the family of subsets C_{A}(a, −) the subset C_{A}(a, ∗) ≡ a^{+}. Thus, we obtain a new axiom-set I′_{A}(−), C′_{A}(−, −) which still satisfies localization condition, axiom monotonicity and •-left monotonicity. So, Pos(−) is a positivity predicate for the cover relation inductively generated by using the axiom-set I′_{A}(−), C′_{A}(−, −).

Whilst impredicatively, the existence of such a predicate defined by coinduction can be easily justified by using Tarski fixed-point theorem, predicatively the justification of its existence requires much more care but it can be given according to the work done by P. Martin-Löf’s, T. Coquand and E. Palmgren (see [Coq96,Pal02]).

2.2 Cartesianity of FTop_{•}^{i} and FTop_{•}^{i−}

From now on we concentrate on the categories of inductively generated formal topologies since they are known to be cartesian (see [CSSV03]).

Proposition 2.11 FTop_{•}^{i} and FTop_{•}^{i−} are cartesian categories.

Proof. In both categories, the terminal object is the formal topology T inductively generated by the empty set of axioms on the set T ≡ {⊤} equipped with the trivial binary operation and with the positivity predicate defined by stating that, for any a ∈ T, Pos(a) ≡ True.

The binary product of the inductively generated formal topologies A and B, whose axiom-sets are respectively I_{A}(−), C_{A}(−, −) and I_{B}(−), C_{B}(−, −), is the formal topology A × B over the set A × B with the binary operation defined by setting

(a_{1}, b_{1}) · (a_{2}, b_{2}) ≡ (a_{1} · a_{2} , b_{1} · b_{2})

the top element defined by setting

⊤_{A×B} ≡ (⊤_{A}, ⊤_{B})

the positivity predicate defined by setting

Pos_{A×B}((a, b)) ≡ Pos_{A}(a) & Pos_{B}(b)

and axiom-set

I((a, b)) ≡ I_{A}(a) + I_{B}(b)
C((a, b), i) ≡ \{ \begin{matrix}C_{A}(a, i_{a}) × \{b\} & if i ≡ inl(i_{a}) \\ \{a\} × C_{B}(b, i_{b}) & if i ≡ inr(i_{b}) \end{matrix}

Note that we did not add localized top, exchange, localized exchange, contraction, localized contraction axioms and the positivity axiom since their validity in the inductively generated cover follows from the presence of the other axioms. Finally, given any inductively generated formal topology C and any continuous relation F from C to A and any continuous relation G from C to B we define

(pairing)  c ⟨F, G⟩ (a, b) ≡ c F a & c G b
(first projection) (a, b) Π_{1} c ≡ (a, b) ◁_{A×B} {(x, y) | x ◁ c}
(second projection) (a, b) Π_{2} d ≡ (a, b) ◁_{A×B} {(x, y) | y ◁ d}

which are respectively the pairing and projection morphisms that make the formal topology A × B a binary product of A and B. □

Now, we turn to consider the properties of continuous relations among inductively generated formal topologies. The following lemmas show that the general conditions defining a continuous relation can be simplified when we are dealing with maps between inductively generated formal topologies.

Lemma 2.12 Let A be a formal topology, B be an inductively generated formal topology and F be a continuous relation from A to B. Then the following conditions are equivalent:

(i) function continuity

(ii) (axiom cont.) \frac{a F b j ∈ J(b)}{a ◁ F^{−}(C(b, j))} and (weak-cont.) \frac{a F b b ◁ d}{a F d}
(iii) (axiom cont.) \frac{a F b j ∈ J(b)}{a ◁ F^{−}(C(b, j))} and (•-cont.) \frac{a F b · d}{a F b} \frac{a F b · d}{a F d}

where J_{B}(−) and C_{B}(−, −) is the axiom-set of the inductively generated formal topology B.

Note that the instance of axiom cont. on the axiom C_{A}(b, j) ≡ b^{+}, for some suitable j ∈ J_{B}(b), is equivalent to function monotonicity.

Lemma 2.13 Let A be a formal topology, B be an inductively generated formal topology and F be a continuous relation from A to B. Then the following conditions are equivalent:

(i) function saturation

(ii) (axiom-sat.) \frac{i ∈ I(a) (∀xεC(a, i)) xF b}{a F b} and (weak-sat.) \frac{a ◁ c cF b}{a F b}
(iii) (axiom-sat.) \frac{i ∈ I(a) (∀xεC(a, i)) xF b}{a F b} and (•-sat.) \frac{a F b}{a · cF b} \frac{c F b}{a · cF b}

where I_{A}(−) and C_{A}(−, −) is the axiom-set of the inductively generated formal topology A.

Note that the instance of axiom-sat. on the axiom C_{A}(a, i) ≡ a^{+}, for some suitable i ∈ I_{A}(a), is equivalent to function positivity.

Finally, we recall the following result linking formal points with continuous relations.

Proposition 2.14 Let A be a formal topology. Then, there is a bijective correspondence between the collection Pt(A) of the formal points of A and the continuous relations from the terminal formal topology T to A.

2.3 Scott formal topologies

The main result of this paper is a proof that Scott formal topologies are exponentiable over inductively generated formal topologies. Let us recall here the definition of Scott formal topology.

Definition 2.15 A formal topology (A, ·, ⊤, ◁, Pos) is called Scott formal topology (or unary •-formal topology) if, for any a ∈ A and U ⊆ A,

a ◁ U if and only if Pos(a) → (∃uεU) a ◁ {u}

Given any formal topology (A, ·, ⊤, ◁, Pos) its unary image Un(A) is the unary •-formal topology Un(A) ≡ (A, ·, ⊤, ◁_{Un}, Pos) where the cover ◁_{Un} is defined by setting:

a ◁_{Un} U ≡ Pos(a) → (∃uεU) a ◁ {u}

It is trivial to see that Scott formal topologies form a full sub-category of FTop_{•}, that we will call unFTop_{•}. Since it is possible to prove that unary topologies are inductively generated (see [CSSV03]), then unFTop_{•} is also a subcategory of FTop_{•}^{i}. While it is obvious that this result trivially holds from an impredicative point of view, it is interesting to note that a predicative proof requires the use of the axiom of choice, which is an immediate consequence of the definition of the Σ-type in Martin-Löf’s Type theory.

Scott formal topologies such that Pos(⊤) holds are distinguishable among formal topologies because the collection of their formal points forms a Scott domain.^{5}

We call scFTop the full subcategory of unFTop_{•} of Scott formal topologies satisfying Pos(⊤). This category is equivalent to the category of the information bases introduced in [SVV96], where an information base differs from a Scott formal topology only for the fact that the cover relation is restricted to a relation between elements of the base. Such an equivalence yields the following results.

Theorem 2.16 ([SVV96,Val03]) scFTop is impredicatively equivalent to the category of Scott domains and Scott continuous functions. Moreover, it is predicatively cartesian closed.

Note also that, on the contrary, the category of unary formal topologies in FTop_{↓}^{i} is not cartesian closed since it is essentially equivalent to the category of algebraic dcpos with bottom.

The next lemma on the product of an inductively generated formal topology with a unary one will be useful in the following.

Lemma 2.17 Consider the binary product of an inductively generated •-formal topology C ≡ (C, ·_{C}, ⊤_{C}, ◁_{C}, Pos_{C}) and a Scott formal topology A ≡ (A, ·_{A}, ⊤_{A}, ◁_{A} , Pos_{A}). Then, if (c, a) ◁_{C×A} W and Pos_{A}(a) hold then there exists a subset W_{1} of C such that c ◁_{C} W_{1} and, for every w_{1}εW_{1} there exists w_{2} ∈ A such that a ◁_{A} w_{2} and (w_{1}, w_{2})εW.

Proof. By induction on the length of the derivation of (c, a) ◁_{C×A} W. □

The definition of continuous relation between formal topologies can be substantially simplified if we restrict our attention to the case of continuous relations from a unary formal topology to a generic one. This simplification is the key for the possibility to define the exponential topology of a unary formal topology over an inductively generated one (see sections 3.1 and 4.1).

Proposition 2.18 Suppose that A is a Scott formal topology and B any •- formal topology. Then a continuous relation from A to B is a binary proposition a F b between A and B which satisfies function totality, weak-saturation, function positivity, function convergence and the following special case of continuity

(unary continuity) \frac{Pos(a) a F b b ◁_{B} V}{(∃vεV) a F v}

5 The positivity predicate is used to express the fact that only bounded compact elements have a supremum. In fact, if we consider a unary •-formal topology whose base elements are all positive, then its formal points form an algebraic lattice.

As we already did in lemma 2.12, the unary continuity condition can be further simplified if the co-domain formal topology is inductively generated.

Lemma 2.19 Let A be a Scott formal topology, B be any inductively generated •-formal topology and F be a continuous relation from A to B. Then unary continuity is equivalent to weak-continuity plus the following condition

(unary axiom continuity) \frac{Pos(a) a F b j ∈ J(b)}{(∃vεC(b, j)) a F v}

3 The construction of the exponential object

After the presentation of the category FTop_{•}^{i} in the previous sections we are now ready to prove the main result of the paper, namely, the exponentiation of unary •-formal topologies over inductively generated ones.

3.1 The exponential topology

Given a Scott formal topology A and an inductive generated one B, we show how to build a formal topology, that we indicate by A → B, whose formal points are (in bijective correspondence with) the continuous relations from A to B. The set A → B of basic neighbourhoods of A → B is the set of lists whose elements are couples in the set Pos_{A} × B ≡ {(a, b) ∈ A × B | Pos_{A}(a)}. The associative binary operation on A → B is the operation of appending two lists. The intended meaning of a list l ∈ A → B is to give a partial information on a continuous relation R from A to B. To indicate that the list l approximates the continuous relation R we introduce the following notation

R ⊩ l ≡ (∀(a, b)ϵl) aRb

where the proposition xϵl is defined by induction on the construction of l by setting xϵnil ≡ False and xϵ(a, b) · l ≡ (x = (a, b)) ∨ xϵl.

The reason to consider only couples in Pos_{A} × B is that function positivity guarantees that every non positive element of A is in relation with every element of B and hence it is useless to keep the information on the nonpositive elements of A.

We also introduce an equivalence relation among lists

l ∼ m ≡ (∀(a, b) ∈ Pos_{A} × B) (a, b)ϵm ↔ (a, b)ϵl

which simply states that l and m contain the same couples.

According to the explanation in section 2.1, to generate the exponential cover we have first to find an axiom-set that specifies the main properties of the cover relation, then we have to add the localized top, exchange, localized exchange, contraction and localized contraction axioms if they are not already derivable, successively we have to define by co-induction the positivity predicate, then we have to add to the axiom-set so far obtained the positivity axiom and finally we generate the cover relation by induction by the rules of reflexivity, •-left and infinity.

The inspiring idea for the axiom-set is to look for those axioms which will force a point of the exponential formal topology to be a continuous relation. Hence, recalling that the intended meaning of l ◁ U is that ext(l) ⊆ Ext(U), that is, every formal point containing l also contains a basic neighbourhood of U, then l ◁ U amounts to state that, for any continuous relation F, if F ⊩ l then there exists mεU such that F ⊩ m. Following this intuition we arrive to state that, for any l ∈ A → B, there are indexes in I(l) for the following subsets of A → B:

(equality-ax.)  C(l, −) ≡ {m}  if m ∼ l
(totality-ax.)  C(l, −) ≡ {m}  if m ∼ (a, ⊤_{B}) · l
(unary convergence-ax.) C(l, −) ≡ {m}  if m ∼ (a, b · d) · l
and (a, b)ϵl, (a, d)ϵl
(weak saturation-ax.) C(l, −) ≡ {m}  if m ∼ (a, b) · l
and (c, b)ϵl, Pos(a), a ◁_{A} c
(weak continuity-ax.) C(l, −) ≡ {m}  if m ∼ (a, d) · l
and (a, b)ϵl, b ◁_{B} d
(unary continuity-ax.) C(l, −) ≡ {m_{v} | v ∈ C(b, j)} if m_{v} ∼ (a, v) · l
and (a, b)ϵl, j ∈ J(b).

The first schema is the formalization of the equivalence between two lists, which is added to satisfy the localization condition, the second schema is the formalization of function totality, the third one of unary convergence, the fourth one of weak-saturation, the fifth one of weak-continuity and the sixth one of unary axiom continuity. It is possible to show that the axioms above form an axiom-set. To these axioms we do not need to add localized top, exchange, localized exchange, contraction and localized contraction axioms since they are already included in the equality axioms. Then, it is not difficult to verify that such an axiom-set satisfies the localization condition.

Now, we have to look for a positivity predicate which satisfies •-left monotonicity and is monotone on the axiom-set considered so far^{6} . Here, we follow the process of turning an inductively generated formal cover into an inductively generated formal topology by defining the positivity predicate by coinduction as described in section 2.1.

6 An alternative way to prove the existence of the exponential topology of A over B in FTop_{•}^{i} is deriving it as a consequence of the general fact that a coreflective subcategory inherits exponentiation (see [MV03] for more details). Thus, it would be sufficient to prove that the formal cover inductively generated by using the axioms here above is the exponential formal cover of A over B in FTop_{•}^{i−}. We do not follow this route to make the paper self-contained as much as possible.

In this way, we arrive at the following co-inductive rules

(•-left monotonicity)  \frac{Pos(l_{1} · l_{2})}{Pos(l_{1})} \frac{Pos(l_{1} · l_{2})}{Pos(l_{2})}
(equality positivity)  \frac{Pos(l) l ∼ m}{Pos(m)}
(totality positivity)  \frac{Pos(l) Pos(a)}{Pos((a, ⊤) · l)}
(unary convergence positivity) \frac{Pos(l) (a, b)ϵl (a, d)ϵl}{Pos((a, b · d) · l)}
(weak-saturation positivity) \frac{Pos(l) Pos(a) a ◁ c (c, b)ϵl}{Pos((a, b) · l)}
(weak-continuity positivity)  \frac{Pos(l) (a, b)ϵl b ◁ d}{Pos((a, d) · l)}
(unary continuity positivity)  \frac{Pos(l) (a, b)ϵl j ∈ J(b)}{(∃yεC(b, j)) Pos((a, y) · l)}

To complete the construction of the axiom-set for the exponential A → B it remains to add the positivity axiom with respect to the obtained positivity predicate. This addition ends the description of the axiom-set to be used to generate the cover relation for the formal topology A → B and so we only have to prove that the resulting formal topology is the exponential topology of A over B.

Theorem 3.1 Scott formal topologies are exponentiable in FTop_{•}^{i}.

Proof. Formally, the statement means that for any Scott formal topology A the functor − × A from FTop_{•}^{i} to FTop_{•}^{i} has got a right adjoint A → − from FTop_{•}^{i} to FTop_{•}^{i}. The required right adjoint maps a formal topology B to the exponential formal topology A → B just defined. The application morphism Ap from A × (A → B) to B is the relation defined by setting, for any a ∈ A, l ∈ A → B and b ∈ B,

(a, l) Ap b ≡ Pos(a) → (l ◁ (a, b) · nil)

while the abstraction morphism is defined by setting, for any continuous relation F from C × A to B and for any c ∈ C and any l ∈ A → B,

c Λ(F) l ≡ (∀(a, b)ϵl) (c, a) F b

In proving that these definitions yield continuous relations, the key difficulties rely in proving that Λ(F) satisfies function continuity with respect to the unary continuity axiom and the positivity axiom. Continuity of Λ(F) with respect to the unary continuity axiom is proved by a suitable application of lemma 2.17 and continuity with respect to the positivity axiom is proved by showing the validity of function monotonicity for Λ(F). To prove the latter we introduce the proposition

Q(m) ≡ (∃x ∈ C) Pos(x) & x Λ(F) m

and prove that it satisfies all of the conditions defining the positivity predicate of A → B. Here we need again lemma 2.17 to prove that Q satisfies unary continuity positivity. Then we can conclude. Indeed, Pos(c) and cΛ(F)l yields Q(l) and hence Pos(l) follows by maximality of Pos. □

Let us remark that the proof of this theorem is valid intuitionistically even in an impredicative approach since no use of the axiom of choice is required.

After this theorem we can prove the following corollary.

Corollary 3.2 Let A be a Scott formal topology and B be any inductively generated •-formal topology. Then, there exists a bijective correspondence between the collection of the formal points of A → B and the collection of the continuous relations from A to B.

Proof. Combine prop. 2.14 with theorem 3.1. □

Note that this bijective correspondence can be explicitly defined as follows. To any formal point Φ of A → B we associate a relation R_{Φ} between A and B defined by setting:

aR_{Φ}b ≡ a ◁ {c ∈ A | (c, b) · nilεΦ}

which can be proved to be continuous. Vice-versa, to any continuous relation R we associate the subset of A → B defined by setting

Φ_{R} ≡ { l ∈ A → B | R ⊩ l}

which can be proved to be a formal point of A → B.

4 Concluding remarks on exponentiation

In this section, we comment our main result and show some applications.

4.1 Why our result is limited to unary formal topologies

It should be clear that all of the conditions on a continuous relation F from a unary formal topology A to an inductively generated one B have in general one of the following shapes, for a, a′ ∈ A, b, b′ ∈ B and V ⊆ B:

\frac{a R b P (a, b, a′, b′)}{a′ R b′}  \frac{a R b Q(a, b, V)}{(∃yεV) a R y}

Now, in section 3.1 we showed how to obtain an axiom out of each kind of condition. In fact, any condition whose shape is

\frac{a R b P (a, b, a′, b′)}{a′ R b′} corresponds to the axiom

l ◁ (a′, b′) · l, provided that (a, b)ϵl and P (a, b, a′, b′)

and any condition whose shape is

\frac{a R b Q(a, b, V)}{(∃yεV) a R y} corresponds to the axiom

l ◁ {(a, y) · l | yεV }, provided that (a, b)ϵl and Q(a, b, V)

Thus, one can define the exponential of an inductively generated formal topology over another one provided that it is possible to express the general conditions on a continuous relation by using one of the shapes above. So far, we have been able to obtain exponentiation only of unary formal topologies both in the context of •-formal topologies and in the context of formal topologies based on a preorder (see [MV02]).

4.2 Exponentiation over formal covers

The proof of exponentiation of Scott formal topologies in FTop_{•}^{i} suggests how to prove exponentiation of Scott formal topologies over inductively generated formal covers.

Theorem 4.1 Scott formal topologies are exponentiable in FTop_{•}^{i−}.

Proof. The exponential topology of a Scott formal topology A over a generic inductively generated formal cover B is the formal cover inductively generated by the axiom-set described in section 3.1 including only equality-ax., totality-ax., unary convergence-ax., weak saturation-ax., weak continuity-ax. and unary continuity-ax. Then, application and abstraction are defined as in theorem 3.1. □

This result constitutes a partial, but completely predicative, version of [Hyl81,Joh84,Sig95]. Indeed, in those papers, if A is a locally compact locale and B is any locale, then the cover for A → B is generated from axioms on a new proposition, denoted by a ≪ f^{∗}(b) in [Hyl81], which represents the collection of locale morphisms f such that a is way-below f^{∗}b. Now, when A is a locale representing a Scott domain, this proposition corresponds exactly to our R ∈ ext((a, b)·nil) since ext((a, b)·nil) is the collection of all the continuous relations R such that a R b.

4.3 Exponentiation over finitary formal topologies

Among inductively generated formal covers one can consider in particular finitary covers [CSSV03], namely formal covers such that

a ◁ U if and only if (∃U_{0} ⊆_{ω} U) a ◁ U_{0}

It is not difficult to see that in FTop_{•}^{i−} the exponentiation of Scott formal topologies with a base of positive elements, that is, of Scott formal topologies whose formal points form an algebraic lattice, restricts to the subcategory of finitary covers. Indeed, to obtain this result we have simply to check that the axioms generating the exponential cover of a unary •-formal topology over a finitary one remain finitary.

4.4 Embedding

The exponential of a Scott formal topology A over any inductively generated •-formal topology B can be embedded into the exponential A → Un(B) of A over the unary image Un(B) of B. Since it is known that the category of Scott formal topologies scFTop is cartesian closed (see [Val03]), then we can prove that A → Un(B) is isomorphic to the Scott formal topology A →_{scFTop} Un(B), that is, the exponential of A over Un(B) according to the exponentiation structure of scFTop as defined in [Val03]. The definition of A →_{scFTop} Un(B) is the following. The base of A →_{scFTop} Un(B) is the same as that of A → Un(B). Its positivity predicate and cover relation are defined, for l ∈ A → B and U ⊆ A → B, as follows:

Pos_{A→_{scFTop}Un(B)}(l) ≡ (∀y ⊑ l) Pos_{A}(⊙_{A}y) → Pos_{B}(⊙_{B}y)
l ◁_{A→_{scFTop}Un(B)} U ≡ Pos_{A→_{scFTop}Un(B)}(l) →

(∃mεU)(∀x ⊑ m)(∃y ⊑ l) ⊙_{A} x ◁_{A} ⊙_{A}y & ⊙_{B} y ◁_{B} ⊙_{B}x

where ⊑ is the sub-list relation defined by setting

y ⊑ l ≡ (∀(a, b) ∈ Pos_{A} × B) (a, b)ϵy → (a, b)ϵl

and the operations ⊙_{A}(l) and ⊙_{B}(l) yield respectively the product of the first components of all the elements in l and the product of the second components of all the elements in l.

Proposition 4.2 In FTop_{•}^{i} the exponential A → B of a Scott formal topology A over an inductively generated formal topology B embeds continuously into the exponential A → Un(B) via the cover relation of A → B. Moreover, A → Un(B) is isomorphic to the exponential of approximable relations A →_{scFTop} Un(B) in scFTop.

Proof. To prove the embedding of A → B into A → Un(B) a key point is to show that unary continuity axiom reduces to weak-continuity axiom. To this purpose it is useful to show that if (a, b)ϵl and Pos(l) then Pos_{B}(b) follows. This is a consequence of a more general fact, namely, that Pos_{A→B} satisfies

(•-monotonicity) \frac{Pos_{A→B}(l) y ⊑ l}{Pos_{A}(⊙_{A}y) → Pos_{B}(⊙_{B}y)}

which can be proved as follows. Suppose that Pos(l), y ⊑ l and Pos_{A}(⊙_{A}y) hold. Then, after applying weak-saturation positivity and unary convergence positivity repeatedly to derive Pos((⊙_{A}y, ⊙_{B}y) · l) from Pos(l), we use unary continuity positivity on the positivity axiom ⊙_{B}y ◁_{B} (⊙_{B}y)^{+} to conclude Pos_{B}(⊙_{B}y).

Finally, to prove that A → Un(B) is isomorphic to A →_{scFTop} Un(B) a key point is to show that the positivity predicate of A → Un(B) is equivalent to the positivity predicate of A →_{scFTop} Un(B) in scFTop and this follows easily by •-monotonicity for Pos_{A→Un(B)}. □

Recalling that there is a bijective correspondence between the collection of the formal points of A → B and the one of the continuous relations from A to B, this embedding means that continuous relations from a Scott formal topology A to an inductively generated •-formal topology B form a subcollection of the collection of the continuous relations from A to Un(B). This is a special case of a more general lifting property of continuous relations. Indeed, since any •-formal topology A continuously embeds in its unary image Un(A), we can prove that every continuous relation from the •-formal topologies A to B can be lifted to a continuous relation from Un(A) to Un(B), as first noted by G. Sambin.

Theorem 4.3 (domain lifting) Let R be a continuous relation from A to B in FTop_{•}. Then, the same relation is also a continuous relation from the associated unary •-formal topologies Un(A) to Un(B). Moreover, the following diagram commutes in FTop_{•}

\xymatrix{A \ar[r]^{R} \ar[d]_{ξ_{A}} & B \ar[d]^{ξ_{B}} \\ Un(A) \ar[r]|{R} & Un(B)}

where, for any a, a′ ∈ A, a ξ_{A} a′ ≡ a ◁_{A} a′, and, for any b, b′ ∈ B, b ξ_{B} b′ ≡ b ◁_{B} b′.

It is interesting to note that this theorem does not hold for unary formal topologies in FTop_{↓} or FTop_{↓}^{i}.

Moreover, note that the assignment of a Scott formal topology to any formal topology does not extend to a functor from the category of •-formal topologies to that of Scott formal topologies since the lifting of a continuous relation is not functorial.

Remark 4.4 The embedding of a formal topology into its unary image and the lifting of continuous relations to unary topologies are the counterparts of the fact that a topological space can be embedded into a Scott domain and that a continuous function can be lifted to an approximable map (see [Sco76]). A lifting of this kind is the key point in [CR00] to prove that the category Top of topological spaces and continuous functions satisfies some weaken notions of exponentiation and hence it is possible to build a locally cartesian closed category out of it. Indeed, Top is not cartesian closed but in [CR00] it is proved that its exact completion turns out to be a locally cartesian closed category.

Acknowledgements. This work is based on so many results in formal topology that we feel to thank all of the people that contributed to it, especially Paolo Virgili, Giovanni Sambin, Silvia Gebellato, Giovanni Curi and Thierry Coquand. We also acknowledge fruitful discussions with Martin Escardo on the general topic of this paper.

References

[BS01] G. Battilotti and G. Sambin. Pretopologies and a uniform presentation of sup-lattice, quantales and frames. Draft, 2001.

[Coq96] T. Coquand. Formal Topology with posets. Manuscript, 1996.

[CR00] A. Carboni and G. Rosolini. Locally Cartesian closed exact completions. Category theory and its applications (Montreal, QC, 1997). J. Pure Appl. Algebra, pages 103–116, 2000.

[CSSV03] T. Coquand, G. Sambin, J. Smith, and S. Valentini. Inductively generated formal topologies. Annals of Pure and Applied Logic, 2003.

[EHar] M. Escardo and R. Heckmann. Topologies on spaces of continuous functions. Topology proceedings., To appear.

[Hyl81] J.M.E. Hyland. Function spaces in the category of locales. Lecture Notes in Mathematics, 871:264–281, 1981.

[Joh82] P.T. Johnstone. Stone spaces. Cambridge University Press, 1982.

[Joh84] P.T. Johnstone. Open locales and exponentiation. Contemporary Mathematics, 30:84–116, 1984.

[JT84] A. Joyal and M. Tierney. An extension of the Galois theory of Grothendieck. Mem. Amer. Math. Soc., 51:no.309, 1984.

[Mar75] P. Martin-Löf. An intuitionistic theory of types: predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium ’73 (Bristol, 1973), volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, Amsterdam, 1975.

[Mar98] P. Martin-Löf. An intuitionistic theory of types. In J. Smith G. Sambin, editor, Twenty five years of Constructive Type Theory, pages 127–172. Oxford Science Publications, 1998.

[MV02] M.E. Maietti and S. Valentini. Exponentiation of unary topologies over inductively generated formal topologies. See http:\\www.math.unipd.it\ ∼silvio\WorkinProg.html, 2002.

[MV03] M.E. Maietti and S. Valentini. Coreflection of formal topologies into formal covers. Preprint, University of Padova, 2003.

[Neg02] S. Negri. Continuous domains as formal spaces. Mathematical Structures in Computer Science., 12:19–52, 2002.

[NPS90] B. Nordström, K. Peterson, and J. Smith. Programming in Martin Löf’s Type Theory. Clarendon Press, Oxford, 1990.

[Pal02] E. Palmgren. Regular universes and formal spaces. Technical Report, University of Uppsala, 42, 2002.

[Sam87] G. Sambin. Intuitionistic formal spaces - a first communication. Mathematical logic and its applications, pages 187–204, 1987.

[Sam03] G. Sambin. Some points in formal topology. Theoretical Computer Science, 2003.

[Sco76] D. Scott. Data types as lattices. Semantics and correctness of programs. SIAM J. Comput., 3:1522–587, 1976.

[Sig95] I. Sigstam. Formal spaces and their effective presentations. Arch. Math. Logic, 34:211–246, 1995.

[SVV96] G. Sambin, S. Valentini, and P. Virgili. Constructive Domain Theory as a branch of Intuitionistic Pointfree Topology. Theoretical Computer Science, 156:319–341, 1996.

[Val03] S. Valentini. A cartesian closed category in Martin-Löf’s intuitionistic type theory. Theoretical Computer Science, 2003.

[Vic01] S. Vickers. The double powerlocale and exponentiation: a case study in geometric logic. Draft, 2001.

[Vir90] P. Virgili. Una categoria cartesiana chiusa delle topologie formali. Tesi di laurea, University of Milano, 1990.