On Fixpoint Objects and Gluing Constructions

Roy L. Crole

             email: rlc3@mcs.le.ac.uk
          http://www.mcs.le.ac.uk/~rlc3

April 21, 1997

Abstract

This article^{1} has two parts:

In the first part, we present some general results about fixpoint objects. The minimal categorical structure required to model soundly the equational type theory which combines higher order recursion and computation types (introduced by [4]) is shown to be precisely a let-category possessing a fixpoint object. Functional completeness for such categories is developed. We also prove that categories with fixpoint operators do not necessarily have a fixpoint object.

In the second part, we extend Freyd’s gluing construction for cartesian closed categories to cartesian closed let-categories, and observe that this extension does not obviously apply to categories possessing fixpoint objects. We solve this problem by giving a new gluing construction for a limited class of categories with fixpoint objects; this is the main result of the paper. We use this category-theoretic construction to prove a type-theoretic conservative extension result.

A version of this paper is due to appear in the Journal of Applied Categorical Structures.

1AMS classification 18 C 10

1 Introduction

We begin by indicating what material readers should be acquainted with. We shall assume that the reader is fully conversant with basic category theory; see, for example, [13], [12], [1] or [2]. In particular, the Yoneda lemma will play a key role in the proof of our main result. This paper also assumes familiarity with the basic philosophy of categorical type theory, namely that there are precise mathematical correspondences between certain kinds of type theories and logics, and appropriate categorical structures. For an introduction to categorical type theory, see for example [12], [2] or [15]. For a deeper treatment of the topic, see [7]. It is well known that the equational theory corresponding to a cartesian closed category is a theory with a unit type, binary product types and function types. That this is well known stems in part from the fact that such a theory amounts to (a version of) the λ-calculus, which has played a prominent role in Computer Science in recent decades. However, many other such correspondences are proving to be useful in the Computer Science community; this paper concentrates on the correspondence between appropriate equational theories, and let-categories with fixpoint objects. Moggi introduced equational theories for let-categories in [14]. The equational theories corresponding to categories with fixpoint objects were introduced in [4]. We shall give a brief summary of the definitions of these categorical structures, and the corresponding equational type theories, in Section 2.

The aims of this paper are twofold. The first goal is to present some miscellaneous results about fixpoint objects. In particular, we are aiming to give some feel for the associated category theory/type theory correspondence. We show that the minimal requirements on a category for it to provide a sound model of the type theory of fixpoints are precisely that the category possess (a strong monad and) a fixpoint object. Continuing this theme, we show how to define polynomial categories over categories with fixpoint objects; our results provide sufficient machinery for the above correspondence to be presented á lá Lambek and Scott. We give an indication of the nature of the recursion which is captured by a fixpoint object by giving an example of a category where (certain kinds of) fixed points abound which can not be characterised using the universal properties of a fixpoint object.

The second goal is to use our categorical machinery to prove a conservative extension result for a type theory. The crux of the proof of this conservative extension appears in the proof of Theorem 6.7, which may be regarded as the most important result of this paper. Note that the techniques used in the proof of Theorem 6.7 are not directly connected with many of the earlier miscellaneous results—those that are used will be clearly indicated.

The layout of this article is as follows:

• In Sections 2 to 4, we give some general results about fixpoint objects. Section 2 provides some background material for the remainder of the paper. Sections 3 and 4 are independent of each other.

• In the second part, Sections 5 to 7, we build up some categorical machinery to prove a certain conservative extension result.

In section 2 we give a summary of the correspondence between let-theories and let-categories, and fix-theories and fix-categories; in particular we derive from first principles the minimal categorical structure required for the sound modelling of a fix-theory. In Section 3 we extend the basic notion of a polynomial category to the situation where the base category is a cartesian closed let-category with a fixpoint object. We prove that in such a set-up, the fixpoint object of the base category embeds to a fixpoint object for the polynomial category. In Section 4 we show that a category which has fixpoints of a certain class of endomorphisms, and for which we might expect the category to be equipped with a fixpoint object, does in fact not have one. In Section 5, we prove an abstract version of the usual gluing lemma for cartesian closed categories, but here for cartesian closed let-categories. In Section 6 we give a new gluing construction for a restricted class of FIX-categories.^{2} Finally, in Section 7, we show how certain type theories generated from an algebraic theory give rise to freely generated categories. We use the categorical machinery developed in Sections 5 and 6 to prove type-theoretic conservative extension results.

2 Categorical Background

The material in this section, apart from Proposition 2.2, provides a summary of those concepts central to the remainder of the paper.

Notation and Conventions

We shall assume that all categories in this article are locally small: all of our constructions are closed under local smallness, and dealing with hom sets makes for a smooth presentation. We shall use the phrase “morphisms A → B” to mean “morphisms with source A and target B.” If F: C → D is a functor and E a category, we write F^{∗}: E^{D} → E^{C} for the functor sending G: D → E to G ∘ F, and define F_{∗}: C^{E} → D^{E} similarly.

Let-Categories and Let-Theories

We recall [3], [4] that a let-category (C, T, η, lift) is simply a category C with finite products which is equipped with an indexed Kleisli triple, that is to say:

• For each object A in C, there is an object T A,

• for each object A in C, there is a morphism η_{A}: A → T A, and

2See page 21.

g ∘ (f × id_{B}) : A × B ⟶ A′ × B ⟶ T C

                                                     \overline{LiftS}

lift(g) ∘ (f × id_{T B}) : A × T B ⟶ A′ × T B ⟶ T C

A × T B
[figure: id × η_{B}; lift(f); LiftB]
A × B  \overline{f  ^{}}T C

η_{B} ∘ π_{2} : A × B ⟶ B ⟶ T B

                                             \overline{LiftH}

π_{2} : A × T B ⟶ T B

lift(g) ∘ ⟨π_{1}, f⟩ : A × B ⟶ A × T C ⟶ T D

                                                     \overline{LiftA}

lift(g) ∘ ⟨π′_{1}, lift(f)⟩ : A × T B ⟶ A × T C ⟶ T D

Figure 1: The Equations of a Let-Category

• for each morphism f: A×B → T C, there is a morphism lift(f): A×T B → T C,

which satisfy certain equations which are given in Figure 1; we shall make use of the notation

{f: A × B ⟶ T C \atop g: A × T B ⟶ T C}

to indicate that g = lift(f).

Recall also that let-categories are simply categories with finite products which are equipped with strong monads—for the latter see [9], [14] and [3]. This is made precise in the following lemma:

Lemma 2.1 If f: B → T C in C then we write

let(f) =^{def} lift(f ∘ π_{B}) ∘ π_{T B}^{−1}: T B → T C

where π_{B}: 1 × B → B and π_{T B}: 1 × T B → T B. Given a let-category C, the corresponding strong monad (T, η, μ, τ) is given by a functor T: C → C sending f: A → B to let(η_{B} ∘ f): T A → T B, a unit η whose components are the η_{A}, a multiplication μ with components μ_{A} =^{def} let(id_{T A}) and a strength

τ : id_{C} × T ⟶ (T ∘ ×) : C × C → C

with components τ_{(A,B)} =^{def} lift(η_{A×B}). Conversely, given a category C with finite products and strong monad, the let-category structure is as expected, with

lift(f) =^{def} μ_{C} ∘ T f ∘ τ_{(A,B)}

if f: A × B → T C in C.

Proof Routine calculations. □

We shall now briefly recall the equational type theory corresponding to letcategories. Judgements will take the form

[x_{1}: α_{1}, …, x_{n}: α_{n}] ⊢ M: α

where each α_{i} and α are types, [x_{1}: α_{1}, …, x_{n}: α_{n}] is an environment (which for us is a list of (variable,type) pairs) and M is a (raw) term. We will usually denote environments by Γ. Such a judgement asserts that in the environment Γ the term M is assigned the type α. We call these judgements typing assertions. Judgements will also take the form

Γ ⊢ M = M′: α

and these assert a formal equality between the two terms M and M′.

A theory [2] page 127, Th, consists (as usual) of a collection of rules for deriving typing assertions and equations between terms. A let-theory contains typing assertions of the form

\frac{Γ ⊢ M: α}{Γ ⊢ Val(M): T α}  \frac{Γ ⊢ E: T α Γ, x: α ⊢ F (x): T β}{Γ ⊢ Let (E, F): T β}

and the let-theory equations are

Γ ⊢ Let (Val(M), F) = F (M)  (1)
Γ ⊢ Let (E, u.Val(u)) = E  (2)
Γ ⊢ Let (Let (E, F), G) = Let (E, u.Let (F (u), G))  (3)

As usual, we write [[−]]: Th → C for the operation giving a structure in a category C to a type theory Th. We can interpret a let-theory in a let-category by defining

[[T α]] =^{def} T ([[α]])
[[Γ ⊢ Val(M): T α]] =^{def} η_{[[α]]}([[Γ ⊢ M: α]])
[[Γ ⊢ Let (E, F): T β]] =^{def} lift([[Γ, x: α ⊢ F (x): T β]])⟨id, [[Γ ⊢ E: T α]]⟩

and the let-theory equations are modelled by the above structure in a let-category.

Fix-Categories and Fix-Theories

We recall the notion of a fixpoint object in a suitably structured category. Given a category C with finite products, the C-indexed category C^{(−)} is specified by:

• The objects of C^{C} are those of C, • C^{C}(A, B) =^{def} C(C × A, B) where composition of g and h in C^{C} is h⟨π, g⟩ in C,

• C^{k}(A) =^{def} A and C^{k}(g) =^{def} g(k × id),

where k: C′ → C in C and A →^{g} B →^{h} D in C^{C}. Note that given a let-category C there is an indexed endofunctor T^{(−)} on C^{(−)} where T^{C}(A) =^{def} T A and T^{C}(g) =^{def} lift(η_{B}g). With this we make the following definition: in a let-category C, a fixpoint object (FPO) is specified by the following data

• An initial T^{(−)} algebra whose structure map in the fibre C^{C} is the morphism C × T Ω →^{π} T Ω →^{σ} Ω in C. Thus given a morphism f: T A → A in C^{C}, there is a unique morphism it(f): Ω → A in C^{C} for which the following diagram commutes (in C):

C × T Ω  \overline{id × σ  ^{}}C × Ω

[figure: C × T A; ⟨π_{C}, lift(η_{A} ∘ it(f))⟩; f; A; it(f)]

• A global element ω: 1 → T Ω which gives rise to an equaliser diagram of the form

[figure: 1; ω; T Ω; η_{Ω}σ; id; T Ω.]

We shall call a let-category equipped with a FPO a fix-category.

A fix-theory [4] consists of typing assertions of the form

\overline{Γ ⊢ ω: T fix}  \frac{Γ ⊢ E: T fix}{Γ ⊢ σ(E): fix}  \frac{Γ, x: T α ⊢ F (x): α Γ ⊢ N: fix}{Γ ⊢ It_{α}(F, N): α}

and equations of the form

Γ ⊢ ω = Val(σ(ω))  (4)
Γ ⊢ E = Val(σ(E)) ⊃ Γ ⊢ E = ω  (5)
Γ, e ⊢ G(σ(e))=F (Let (e, n.Val(G(n)))) ⊃ Γ ⊢ G(N) = It_{α}(F, N)  (6)
Γ ⊢ It_{α}(F, σ(E)) = F (Let (E, n.Val(It_{α}(F, n))))  (7)

It is instructive to show that, subject to the usual paradigm of categorical type theory that substitution is interpreted by composition and rule formation by natural transformations [2], the minimal structural requirements of a category C for the sound modelling of a fix-theory are that C be a let-category with FPO. This is our first proposition:

Proposition 2.2 In order to model a fix-theory in a category C, the minimal requirements of C are that it is a let-category which is endowed with a FPO.

Proof We shall need an object Ω of C to model fix, that is [[fix]] =^{def} Ω. To interpret the first typing assertion, we shall need a global element of T Ω. So we have

[[Γ ⊢ ω: T fix]] =^{def} ω∘!: [[Γ]] → 1 → T Ω,

where [[Γ]] is the usual finite product of the interpretations of the types in Γ. To interpret the second typing assertion, with the usual assumptions about the way we shall model substitution, we shall need a natural transformation

θ: C(−, T Ω) → C(−, Ω).

Using the Yoneda Lemma, we can deduce that the effect of the components θ_{C} arise by post composition with a morphism σ: T Ω → Ω. Thus we can set

[[Γ ⊢ σ(E): fix]] =^{def} θ_{[[Γ]]}(e) = σ ∘ e,

where, by structural induction we already have [[Γ ⊢ E: T fix]] = e. To interpret the third typing assertion, we shall need a natural transformation with components

θ_{C}: C(C × T A, A) × C(C, Ω) \overline{}C(C, A).

Applying naturality to ⟨id, n⟩: C → C × Ω, we get

θ_{C}(f, n) = θ_{C×Ω}(f ∘ (π_{1} × id), π_{2}) ∘ ⟨id, n⟩

where π_{1}: C × Ω → C and π_{2}: C × Ω → Ω. Thus it is enough to model the third typing assertion if we have a natural transformation which has components

ϕ_{C}: C(C × T A, A) \overline{}C(C × Ω, A).

Writing it(f) =^{def} ϕ_{C}(f), we may define

[[Γ ⊢ It(F, N): α]] =^{def} it(f) ∘ ⟨id, n⟩,

where we already have

[[Γ, x: T α ⊢ F (x): α]] = f
[[Γ ⊢ N: fix]] = n.

Now we consider the equations of a fix-theory. It is easy to see that for the sound modelling of (4) and (5) it is necessary and sufficient that the triple (ω, σ, Ω) satisfies the equaliser requirement of a FPO.

Note that using the usual logical rules of equational type theory, rule (6) is equivalent to

Γ, e ⊢ G(σ(e)) = F (Let (e, n.Val(G(n)))) ⊃ Γ, n ⊢ G(n) = It_{α}(F, n) (8)

In order to model (8) we see it is necessary that^{3}

g(id × σ) = f⟨π_{1}, lift(ηg)⟩
(∗)
g = it(f)

where f: C × T A → A, g: C × Ω → A and π_{1}: C × T Ω → C; sufficiency of the uniqueness requirement of a FPO is immediate.

Finally, we look at the structure needed to model (7). Put

π_{2}: C × T Ω → T Ω π_{3}: C × Ω → C π_{4}: C × Ω → Ω.

Working through the details we shall need

it(f)(id × σ)⟨id, e⟩ = f⟨id, lift(it(η(f(π_{3} × id)))⟨id, π_{4}⟩)⟨id, e⟩⟩  (9)

where e: C → T Ω. However, we can appeal to (∗) to deduce that it((f(π_{3} × id))) = it(f)(π_{3} × id); thus (9) reduces to

it(f)(id × σ)⟨id, e⟩ = f⟨id, lift(η ∘ it(f))⟨id, e⟩⟩.  (10)

The universal property of a FPO is certainly sufficient to ensure that (10) holds. To see that it is also necessary, note that

f⟨π_{1}, lift(η ∘ it(f))⟩ = f(π_{1} × id)⟨id, lift(η ∘ it(f)(π_{1} × id))⟨id, π_{2}⟩⟩
= f(π_{1} × id)⟨id, lift(η ∘ it((f(π_{1} × id))))⟨id, π_{2}⟩⟩
using an instance of (10) = it((f(π_{1} × id)))(id × σ)⟨id, π_{2}⟩
= it(f)(π_{1} × id)(id × σ)⟨id, π_{2}⟩
= it(f)(id × σ).

Finally note that the universal property of a FPO ensures Ω and σ are determined up to isomorphism. □

A few remarks are in order. The basic definition of FPO requires the structure of a let-category. However, an equivalent, but much simpler definition, can be given in the presence of cartesian closure. For convenience, from now on we shall always deal with let-categories C which are also cartesian closed; such a category will be referred to as a let-ccc. Recall [4] that a fixed point object (FPO) (Ω, σ, ω) in a let-ccc amounts to specifying an initial T -algebra for the functor T, say σ: T Ω → Ω, together with a global element ω of T Ω which is the equaliser of η_{Ω} ∘ σ and id_{T Ω}. (See [4] for the proof that this definition is equivalent to that given on page 6.)

Let us look at an example, which will play a key role in Section 6. It is well known that ωCPO, the category of ωcpos (not necessarily with bottom) and Scott continuous functions, is a let-ccc (ωCPO, (−)_{⊥}, ι, lift(−)) where • D_{⊥} =^{def} {[d] | d ∈ D} ∪ {⊥} for an ωcpo D is the lifted ωcpo,

3In the remainder of this paper, we omit most composition symbols ∘, writing uv for u ∘ v, and often omit sub-scripts from natural transformations (e.g. η: A → T A).

• ι_{D}: D → D_{⊥} is defined by d ↦ [d], and

• if f: D × D′ → D′′_{⊥} is Scott continuous, then lift(f): D × D′_{⊥} → D′′_{⊥} is defined by (d, ⊥) ↦ ⊥ and (d, d′) ↦ f(d, d′). We shall write f_{⊥} for let(f) in ωCPO.

Moreover, ωCPO has a FPO (σ, ℕ^{∞}, [∞]) where ℕ^{∞} is the vertical natural numbers with top element ∞, and σ: ℕ_{⊥}^{∞} → ℕ^{∞} is the function defined by σ(⊥) = 0, σ([n]) = n + 1 and σ([∞]) = ∞.

Freely Generated Categories

In Section 7 we shall make use of freely generated categories; here we clarify our definition of this concept. Suppose that struc refers to a categorical structure (for example cartesian closure, possessing a strong monad and so on). Then a morphism of struc-categories is a functor which preserves the structure. If the structure is a property of the category, this notion is standard. We clarify our definition as applied to strong monads (let structures) which are, of course, not categorical properties but chosen structures. A morphism of let-categories (C, T) → (D, S) is a monad morphism (F, i) between the underlying monads for which the functor F: C → D preserves finite products, and each i: F (T C) ≅ S(F C) is a natural isomorphism. Thus to be given a let-category morphism (F, i): (C, T) → (D, S) means for each object A in C we are given an isomorphism i_{A}: F T A ≅ SF A which is compatible with the remaining structure. For example, suppose we are given a morphism f: A×B → T C in C. Then there is a morphism

g: F A × F B ≅ F (A × B) ⟶^{F f} F T C ⟶^{i_{C}} SF C

and a morphism

h: F A × F T B ≅ F (A × T B) ⟶^{F (lift(f))} F T C

for which, by definition, the following diagram commutes:

[figure: F A × SF B; lift(g); SF C; F A × F T B; id × i_{B}; h; F T C; i_{C}]

The (categorical) isomorphisms are, of course, the canonical ones.

Let C be a category with finite products. Then FC is the freely generated struccategory on C if there is a functor I: C → FC such that (i) I preserves finite products,

(ii) if D is any struc-category, and F: C → D preserves finite products, then there is a morphism \overline{F}: FC → D of struc-categories for which there is a natural isomorphism ϕ: \overline{F} ∘ I ≅ F, and

(iii) if also ϕ′: \overline{\overline{F}} ∘ I ≅ F where \overline{\overline{F}}: FC → D also satisfy (ii), then there is a natural isomorphism ψ: \overline{F} ≅ \overline{\overline{F}} for which ψ_{I} = ϕ^{′−1} ∘ ϕ.

3 Functional Completeness

In this section we shall prove that the polynomial category of a let-ccc is functionally complete. We refer to page 59 of [12] for a similar discussion concerning cartesian closed categories. We also show that if a let-ccc has a FPO, this embeds to a FPO in the associated polynomial category. These results are presented for their own inherent interest, and because the category theory/type theory correspondence can be presented using the notion of polynomial categories; in particular, our results show that the approach of Lambek and Scott [12] (page 77 onwards) to such a correspondence applies in our setting.

We begin with the definition of let-ccc polynomial categories. Note that the definition of these categories is simple, but should be treated with care^{4} and so we spell out the details. Let C be a let-ccc and let E be an object of C. The polynomial let-ccc C[X] in variable X for E is specified by the following data:

• The objects of C[X] are just the objects of C.

• We set mor C[X] =^{def} ⟨PM ⟩/ ∼ where

(i) PM =^{def} mor C ∪ {X},

(ii) ⟨PM ⟩ is generated from PM via the (formal) rules

{f: A → B ∈ PM \atop f: A → B ∈ ⟨PM ⟩}  {u: A → B ∈ ⟨PM ⟩ v: B → C ∈ ⟨PM ⟩ \atop v ∘ u: A → C ∈ ⟨PM ⟩}

{u: A → B ∈ ⟨PM ⟩ v: A → C ∈ ⟨PM ⟩ \atop ⟨u, v⟩: A → B × C ∈ ⟨PM ⟩} {u: A × B → C ∈ ⟨PM ⟩ \atop λ(u): A → (B ⇒ C) ∈ ⟨PM ⟩}

u: A × B → T C ∈ ⟨PM ⟩
lift(u): A × T B → T C ∈ ⟨PM ⟩

(iii) ∼ is the equivalence relation generated by 1. If f = g in C, then f ∼ g.

4Thanks to Martin Hyland for making me realise just how careful one needs to be!

2. u ∘ id ∼ u ∼ id ∘ u.

3. If u ∼ u′ and v ∼ v′, then v ∘ u ∼ v′ ∘ u′.

4. (w ∘ v) ∘ u ∼ w ∘ (v ∘ u).

5. Conditions forcing (formal) cartesian closure of C[X]; see [12], page 57.

6. If u ∼ u′ then lift(u) ∼ lift(u′).

7. Conditions forcing C[X] to be a let-category; for example, this amounts

to requiring

lift(v ∘ (u × id)) ∼ lift(v) ∘ (u × id),

corresponding to LiftS (see page 4); similar conditions hold for the other let structure equations. Here, of course, u × id =^{def} ⟨u ∘ π, π′⟩.

• If u ∈ ⟨PM ⟩ we write [u] for the equivalence class of u in mor C[X]. The source of^{5} [X] is defined to be 1 and the target E; then the source-target predicate in C[X] is the expected one. The identity on A is [id_{A}], and composition in C[X] is given by [u] · [v] =^{def} [u ∘ v]. Note that (1) to (4) ensure that C[X] is indeed a category and that there is an obvious functorial embedding ι: C ↪ C[X].

Proposition 3.1 For the above data, C[X] is a let-ccc with projections [π]: A × B → A, pairing ⟨[u], [v]⟩ =^{def} [⟨u, v⟩], and the let-structure given by A ↦ T A on objects, units [η_{A}]: A → T A, and lift([u]) =^{def} [lift(u)] for a morphism [u]: A×B → T C in C[X].

Proof The cc-stucture is standard [12]. We check (for example) that LiftS holds:

lift([u]) · ([v] × id_{T B}) = [lift(u)] · ⟨[v] · [π], [π′]⟩
= [lift(u)] · [⟨v ∘ π, π′⟩]
= lift([u] · ([v] × id_{B})).

The other details are routine computations. □

Proposition 3.2 The polynomial category is characterized by the following universal property: Suppose that ι: C ↪ C[X] is the embedding described above. Let D be a let-ccc, F: C → D a morphism of let-cccs and d: F 1 → F E any morphism in D. Then there is a unique morphism of let-cccs \overline{F}: C[X] → D such that

C  \overline{ι ^{}}C[X]
[figure: \overline{F}]
D^{F^{}}

commutes with \overline{F} ([X]) = d.

5Note that C[X] denotes the polynomial category, but that [X] denotes the equivalence class of the symbol X in ⟨PM ⟩/ ∼.

Proof The proof details are essentially routine, where \overline{F} is F on the objects of C[X], and defined recursively on the morphisms of C[X] through the rules specifying mor C[X]. \overline{F} ([X]) =^{def} d is of course a base clause for the recursive definition. □

Remark 3.3 We shall write just u rather than [u] for morphisms in the polynomial category, and write uv for composition rather than [u] · [v].

Now we prove a version of functional completeness for let-cccs:

Theorem 3.4 Let C be a let-ccc and C[X] its polynomial category. For every morphism u: B → C in C[X] there is a unique morphism

Λ(u): E × B → C

in C such that

Λ(u)⟨X!, id⟩ = u

where !: B → 1. In particular, each global element of C in C[X] is of the form fX for some unique morphism f: E → C in C.

Proof As there is a proof of this result for cccs in [12], page 59, we just give details of the proof for the let structure. Take morphisms

u : B × B′ → T C,
and hence lift(u) : B × T B′ → T C,
l : (E × B) × B′ → E × (B × B′),
m : E × (B × T B′) → (E × B) × T B′,

where l and m are the obvious isomorphisms. By induction, we shall assume that there is a morphism

Λ(u): E × (B × B′) → T C

that satisfies functional completeness. Then we define

Λ(lift(u)) =^{def} lift(Λ(u)l)m,

and refer the reader to [12], page 51, for the definition of Λ on the ccc structure. We have to check that this is well defined, i.e. if u ∼ v in C[X] then Λ(u) ∼ Λ(v) in C[X]. This amounts to showing that Λ respects each of conditions (1) to (7) of Definition 3; most of these are easy to verify, but we check in detail one of the let-structure conditions of (7), namely lift(v⟨uπ, π′⟩) ∼ lift(v)⟨uπ, π′⟩. We have

Λ(lift(v⟨uπ, π′⟩)) ∼ lift(Λ(v⟨uπ, π′⟩)l)m
by definition is ∼ lift(Λ(v)⟨π, ⟨Λ(u)⟨π, ππ′⟩, π′π′⟩⟩⟨ππ, ⟨π′π, π′⟩⟩)m
which is ∼ lift(Λ(v)⟨ππ, ⟨Λ(u)π, π′⟩⟩)m
for appropriate l′ ∼ lift(Λ(v)l′(⟨π, Λ(u)⟩ × id))m
from the let structure ∼ lift(Λ(v)l′)(⟨π, Λ(u)⟩ × id)m
∼ lift(Λ(v)l′)m′⟨π, ⟨Λ(u)⟨π, ππ′⟩, π′π′⟩⟩
∼ Λ(lift(v))⟨π, Λ(⟨uπ, π′⟩)⟩
∼ Λ(lift(v)⟨uπ, π′⟩)

which is what we had to show. Now that we know Λ is well defined we prove the result itself. Indeed,

Λ(lift(u))⟨X!, id⟩ = lift(Λ(u)l) ∘ m ∘ ⟨X!, id⟩
= lift(Λ(u)l) ∘ (⟨X, id⟩ × id)
by LiftS for the let-ccc C[X] = lift((Λ(u)l) ∘ (⟨X!, id⟩ × id))
= lift(Λ(u) ∘ ⟨X!, id⟩)
and by induction = lift(u).

It remains to prove uniqueness. Suppose that there is g: E × B → C for which g⟨X!, id_{B}⟩ = u. We have to show that g = Λ(u). This follows from the following computation:

Λ(u) = Λ(g⟨X!, id⟩)
= Λ(g)⟨π, Λ(⟨X!, id⟩)⟩
= gπ′⟨π, Λ(⟨X!, id⟩)⟩
= gΛ(⟨X!, id⟩)
= g⟨Λ(X!), Λ(id)⟩
= g⟨π, π′⟩
= g ∘ id_{E×B}
= g.

(Again we emphasise that the definition of Λ on the ccc structure of C[X] can be found on page 51 of [12].) □

Proposition 3.5 Let C be a let-ccc with FPO Ω. Then C[X] also has a FPO, given by Ω = i(Ω), where i : C ↪ C[X] is the canonical inclusion functor.

Proof Consider the diagram in C[X] given in Figure 2, where σ: T Ω → Ω is the embedding of the FPO of C in C[X], f is any morphism T B → B in C[X], and where k =^{def} ⟨π_{E}, lift(η ∘ it(Λ(f)))⟩.

We set h =^{def} it(Λ(f))⟨X!, id⟩, where the morphism Λ(f) is defined by appealing to Theorem 3.4. In order to prove that hσ = flet(ηh) we inspect the diagram above. It is clear all regions commute except for k⟨X!, id⟩ = ⟨X!, id⟩let(ηh). To prove this it is enough to show that lift(η ∘ it(Λ(f)))⟨X!, id⟩ = let(η ∘ it(Λ(f))⟨X!, id⟩). We appeal to Theorem 3.4 and note

Λ(let(η ∘ it(Λ(f))⟨X!, id⟩)) = lift(Λ(η ∘ it(Λ(f)))⟨π, Λ(⟨X!, id⟩)⟩)
= lift(ηπ′⟨π, it(Λ(f))π′⟩⟨π, ⟨π, π′⟩⟩)
= lift(η ∘ it(Λ(f))⟨π, π′⟩).

It remains to prove uniqueness. Suppose also that gσ = flet(ηg). Note that if Λ(g) = it(Λ(f)) then h = it(Λ(f))⟨X!, id⟩ = Λ(g)⟨X!, id⟩ = g; so it is sufficient to

T Ω  \overline{σ  ^{}}Ω
[figure: ⟨X!, id⟩; ⟨X!, id⟩]
E × T Ω \overline{id × σ_{}}E × Ω

[figure: E × T B; k; Λ(f); B; it(Λ(f)); =; B; . . . . . . . . . . . . . . . . . . . . . .; h]
[figure: ⟨X!, id⟩]
T B^{let(ηh)^{}. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .}  \overline{f  ^{}}B^{^{}= }

Figure 2: A Diagram Used in the Proof of Proposition 3.5

prove the former. For this, if we can show Λ(g)(id × σ) = Λ(f)⟨π_{E}, lift(ηΛ(g))⟩ we are done using the universal property of the FPO Ω in C. As Λ(gσ) = Λ(g)(id × σ) it is sufficient to prove Λ(f)⟨π_{E}, lift(ηΛ(g))⟩⟨X!, id⟩ = gσ. We have

Λ(f)⟨π_{E}, lift(ηΛ(g))⟩⟨X!, id⟩ = Λ(f)⟨X!, lift(ηΛ(g))⟨X!, id⟩⟩
using uniqueness of Λ(−) = Λ(f)⟨X!, let(ηg)⟩
= flet(ηg)

and so we are done. Finally, the equaliser condition is simple to verify. □

4 A Category with Fixpoints, without a Fixpoint Object

A domain [16] is usually defined to be a poset with some form of cocompleteness property, that is, joins of certain kinds are required to exist. Categories of domains arise naturally as suitable arenas in which to give semantics to programming languages, but that does not concern us here [6]. One reason for this is that the existence of fixed point operators in such categories can be used to give semantics to recursive program declarations. Turning to more theoretical issues, we might ask if it is always the case that a concrete category of domains has a FPO whenever the morphisms between lifted domains may be guaranteed to have fixpoints. This is not so, and is the central result of this section. We present it because it shows clearly that the properties captured by abstract FPOs are quite closely tied to the usual concrete models of recursion.

Let OnCPO be the category which has

• objects posets possessing suprema of all chains and

• morphisms monotone set functions.

It is easy to see that this category is indeed a let-ccc when we regard the lifting functor as giving rise to a strong monad. It is the case that all morphisms f: D_{⊥} → D_{⊥} have a least fixpoint. For given any such morphism f, define for any ordinal α the element f^{α}(⊥) by

f^{0}(⊥) = ⊥
f^{α+1}(⊥) = f(f^{α}(⊥))
f^{λ}(⊥) = ⋁_{α<λ} f^{α}(⊥) where λ is a limit ordinal.

This is a good definition. The only thing that is not trivial is the existence of f^{λ}(⊥): the set {f^{α}(⊥) | α < λ} must be a chain. But a simple transfinite induction shows that α ≤ α′ < λ implies f^{α}(⊥) ≤ f^{α′}(⊥). Next note that there is some ordinal β for which f^{β}(⊥) is a least fixpoint of f. Suppose this were not the case. By appealing to Hartog’s Lemma, we can find a least ordinal (say γ) whose cardinality is strictly greater than the cardinality of the domain of f, say |D_{⊥}|. Using the hypothesis, it must be the case that the cardinality of {f^{α}(⊥) | α ≤ γ} is strictly greater than |D_{⊥}|, a contradiction.

Theorem 4.1 The let-ccc OnCPO does not possess a fixpoint object for the lifting monad.

Proof Let us suppose that the fixpoint object Ω exists in OnCPO. We write i: Ω ↪ Ω_{⊥}, n ↦ [n] for the (monic) component of the unit of the lifting monad at Ω. From the equaliser condition of the fixpoint object, iσ: Ω_{⊥} → Ω_{⊥} has a unique fixpoint (which cannot be bottom), say [⊤] ∈ Ω_{⊥}. From remarks above there is an ordinal β for which (iσ)^{β}(⊥) = [⊤]; note that β > 1.

We write σ^{1} for σ(⊥), σ^{α+1} for σ([σ^{α}]) and σ^{λ} for ⋁_{α<λ} σ^{α}; note that each supremum exists.

The ordinals ω + 2 and ω + 1 are objects of OnCPO; we take ω =^{def} {1, 2, …}. Define a morphism f: (ω + 2)_{⊥} → ω + 2 by setting

f(x) =^{def} \{ \begin{matrix}1 & if x = ⊥ \\ n + 1 & if x = [n] \\ ω & if x = [ω] \\ ω + 1 & if x = [ω + 1] \end{matrix}

and a morphism f_{r}: (ω + 1)_{⊥} → ω + 1 to be f with restricted (co)domain.

Consider the following diagram in which j is inclusion:

Ω_{⊥}  \overline{σ ^{}}Ω

(1)

[figure: (ω + 1)_{⊥}; ^{f̃_{r}^{⊥}}; f_{r}; ω + 1; f̃_{r}]

(2)

[figure: (ω + 2)_{⊥}; j_{⊥}; f; ω + 2; j]

(1) commutes using the universal property of a FPO, (2) trivially. Similarly, there is f̃: Ω → ω + 2 making

Ω_{⊥}  \overline{σ ^{}}Ω

(3)

[figure: (ω + 2)_{⊥}; f̃_{⊥}; f; ω + 2; f̃]

commute. From uniqueness, f̃ = jf̃_{r}. We shall now consider the cases when β is strictly less than, or greater than, ω. In the latter case we obtain a contradiction by defining a morphism different from f̃ which makes (3) commute.

(Case 1 < β < ω): By chasing (1) we see that for any finite ordinal k, f̃_{r}(σ^{k}) = k. From the definition of β it is easy to see that σ^{β} = ⊤. Chasing (1) at [⊤] ∈ Ω_{⊥} we get

β = f̃_{r}(⊤) = f̃_{r}σ([⊤]) = f_{r}f̃_{r}_{⊥}([⊤]) = f_{r}([f̃_{r}(⊤)]) = β + 1

a contradiction. Hence we must have

(Case ω ≤ β): Certainly σ^{k} ≤ σ^{ω} for any finite ordinal k, and so k = f̃_{r}(σ^{k}) ≤ f̃_{r}(σ^{ω}). Hence f̃_{r}(σ^{ω}) = ω. As σ^{β} = ⊤ we have ω = f̃_{r}(σ^{ω}) ≤ f̃_{r}(⊤) and so f̃_{r}(⊤) = ω.

Define a function F: Ω → ω + 2 by

F (n) =^{def} \{ \begin{matrix}ω + 1 & if ⊤ ≤ n \\ f̃(n) & otherwise \end{matrix}

Note that F (⊤) = ω + 1 and f̃(⊤) = jf̃_{r}(⊤) = ω, that is F ≠ f̃. It is the case that F is monotone:

1. On elements of Ω not greater than ⊤, F is monotone for f̃ is.

2. If ⊤ ≤ n ≤ n′ in Ω then F (n) = F (n′).

3. If n ≤ n′ in Ω where n′ is greater than ⊤ but n is not, then F (n) ≤ ω + 1 = F (n′).

Finally, F makes the square (3) commute.

1. Clearly σ^{1} ≤ ⊤ and σ^{1} cannot be ⊤. So F σ(⊥) = f̃(σ^{1}) = 1 = fF_{⊥}(⊥).

2. Suppose [n] ∈ Ω_{⊥} and n is greater than ⊤. Then ⊤ = σ([⊤]) ≤ σ([n]). So

F σ([n]) = ω + 1 = f([F (n)]) = fF_{⊥}([n]).

3. Suppose [n] ∈ Ω_{⊥} and n is not greater than ⊤. Then σ([n]) is not greater than ⊤, for if so, as σ is an isomorphism, [⊤] = σ^{−1}(⊤) ≤ [n] and this is not so. Hence,

F σ([n]) = f̃(σ([n])) = f(f̃_{⊥}([n])) = f([f̃(n)]) = f([F (n)]) = fF_{⊥}([n]).

By the uniqueness criterion, we have F = f̃. This is not so. Hence there can be no fixpoint object in OnCPO, as claimed. □

5 Gluing for Cartesian Closed Let-Categories

Our aim now is to investigate to what extent the gluing construction of Freyd applies in the setting of categories with FPOs. This is interesting in itself, but in particular we are aiming to use such methods to prove a conservative extension result in Section 7. The technique of gluing originated with Freyd, who used it to present a neat method for proving the existence and disjunction properties of certain intuitionistic type theories. His proof made use of a certain topos E manufactured from two other toposes; E is the so-called glued topos and for an account of this see [12], page 237. Other information about gluing (sometimes called sconing) can be found in [8], [11], [10], [5], page 190 and [2], page 185.

As a first step towards our goal, we show that the gluing construction for cccs can be extended to let-cccs:

Theorem 5.1 Let Γ: D → C be a functor where D is a let-ccc and C is a ccc. Suppose also that C has pullbacks and that Γ preserves finite products. Write GL(Γ) for the comma category (C ↓ Γ) and note that there is an obvious functor π_{2}: GL(Γ) → D. Then it is the case that

1. GL(Γ) is a let-ccc, and

2. π_{2} is a morphism of let-cccs.

Proof It is a well known result (see, for example, [10] or [2], page 189) that GL(Γ) is a ccc . We shall denote a typical morphism in GL(Γ) by

(a, s): (A, f, D) → (B, g, D′).

Recall that to be a let-ccc is not a property of the category, but a chosen structure. By the statement that GL(Γ) is a let-ccc, we mean that there is a canonical choice of this structure. We make the following definitions:

1. T (A, f, D) =^{def} (A, Γ(η) ∘ f, T D).

2. η_{(A,f,D)} =^{def} (id_{A}, η_{D}): (A, f, D) ⟶ T (A, f, D).

3.

\frac{(a, s): (A, f, D) × (B, g, D′) ⟶ T (C, h, D′′)}{lift(a, s) =^{def} (a, lift(s)): (A, f, D) × T (B, g, D′) ⟶ T (C, h, D′′)}

Some readers may prefer to see the definition of the strong monad; the multiplication is given by

μ_{(A,f,D)} =^{def} (id_{A}, μ_{D})

and the strength is given by

τ_{((A,f,D),(B,g,D′))} =^{def} (id_{A×B}, τ_{(D,D′)}).

Definitions (1) and (2) clearly make sense. We note that definition (3) is good:

[figure: A × B; f × g; ΓD × ΓD′; ≅; Γ(D × D′); Γ(id × η); Γ(D × T D′)]

[figure: C; a; h; ΓD′′; Γ(η); ΓT D′′; Γ(s); =; ΓT D′′; Γ(lift(s))]

We have to verify that the equations of a let-category (see page 4) hold. We just check one of them: Take morphisms

(a, s): (C, h, D′′) × (A, f, D) ⟶ T (B, g, D′)
(b, t): (C, h, D′′) × (B, g, D′) ⟶ T (E, k, D′′′)
(π, π′): (C, h, D′′) × (A, f, D) ⟶ (C, h, D′′).

Consider the commutative diagram in Figure 3. From this, it is easy to see that

lift(lift(b, t) ∘ ⟨(π, π′), (a, s)⟩) = lift(lift(b, t) ∘ (⟨π, a⟩, ⟨π′, s⟩))
and using the diagram = lift(b, t) ∘ (⟨π, a⟩, ⟨π′, lift(s)⟩)
= lift(b, t) ∘ ⟨(π, π′), (a, lift(s))⟩.

This is exactly LiftA for the glued category GL(Γ). It is immediate that π_{2} is a morphism of let-cccs. □

[figure: C × A; ⟨π, a⟩; C × B; b; E]
[figure: h × f]
[figure: ΓD′′ × ΓT D; h; id×Γ(η); ΓD′′ × ΓD; ΓD′′ × ΓT D′; h × (Γ(η) ∘ g)]
Γ(D′′ × D) [figure: ≅]
[figure: Γ(id × η); Γ(⟨π′, s⟩)]
[figure: Γ(D′′ × T D); ≅; Γ(⟨π′, lift(s)⟩); Γ(D′′ × T D′); ≅; Γ(lift(t)); ΓT D′′′; Γ(η) ∘ k]

Γ(D′′ × T D)

‖
Γ(lift(lift(t)⟨π′, s⟩))  ^{}
ΓT D′′′

‖

Figure 3: A Diagram Used in the Proof of Theorem 5.1

We use the theorem on gluing to prove the following corollary: please see Remark 7.3 for comments on the use of this result. We refer to the proof of Corollary 5.2 in the proof of Corollary 6.8.

Corollary 5.2 Let C be a locally small category, and FC the freely generated let-ccc. Then the canonical functor I: C → FC is full and faithful.

Proof Let Γ be the composite

(I^{op})^{∗} ∘ Y : FC ⟶ Set^{FC^{op}} ⟶ Set^{C^{op}}

where Y is the Yoneda embedding. Thus, by definition, if D is an object of FC, then ΓD is the object of Set^{C^{op}} given by

C^{op} ⟶^{I^{op}} FC^{op} ⟶^{Y D} Set.

One can see that Γ preserves finite products, because both Y and I do. We may define a functor

J: C ⟶ GL(Γ)

by setting JC =^{def} (Y C, γ^{C}, IC) and Jc =^{def} (Y c, Ic), where the component of the natural transformation γ^{C} at an object C′ of C is a function

γ_{C′}^{C}: C(C′, C) ⟶ FC(IC′, IC)

given by c ↦ Ic. Consider the diagram

FC = = = = = = = = FC
[figure: I]
[figure: C; J; GL(Γ); \overline{J}]
[figure: I]
[figure: FC; π_{2}; = = = = = = = =; FC; ^{id^{FC}}]

The functor J preserves products because both I and Y do. Thus the functor \overline{J} exists because Theorem 5.1 says that GL(Γ) is a let-ccc. The diagram does indeed commute: The upper triangle commutes up to (canonical) isomorphism using property (ii) of FC. The lower triangle commutes up to strict equality for trivial reasons. The rectangle commutes up to (canonical) isomorphism from property (iii) of FC because π_{2} is a morphism of let-cccs.

It follows that \overline{J} is faithful for trivial reasons. Thus I will be full and faithful if we can show that J is, which we now do.

That Y is faithful clearly implies that J is too. It remains to show that J is full which takes a little effort. Suppose that (ϕ, h): JC → JC′ in GL(Γ). We need to find c: C → C′ in C such that Jc =^{def} (Y c, Ic) = (ϕ, h). Now, ϕ: Y C → Y C′, and it is standard (from the proof that Y is full) that ϕ = Y (ϕ_{C}(id_{C})) (see page 11 of [12]). Set c =^{def} ϕ_{C}(id_{C}). We are done if h = Ic. In fact this follows from the fact that (ϕ, h) is a morphism in GL(Γ), that is, the diagram

[figure: Y C; ϕ; Y C′; ΓIC; γ^{C}; Γh; ΓIC′; γ^{C′}]

commutes. One needs to take components of the diagram at C, and trace the diagram for id_{C} ∈ (Y C)C = C(C, C), which yields h = I(ϕ_{C}(id_{C})) = Ic. □

6 Gluing for FIX-Categories

As remarked at the start of Section 5, our aim is to consider the gluing construction for categories with FPO. However, we might also consider categories with other structure, such as coproducts and natural numbers objects (NNOs). Indeed, in Section 7 it will be crucial that we can deal with such additional structure. We shall refer to cartesian closed categories with finite coproducts, NNO and FPO as FIX-categories. The author is of the opinion that this name is not ideal. However, as it was used in the reference [4], which is the original source for the current work, we shall stick with it.

We would like to be able to prove a variant of the gluing construction for the case of a finite product preserving functor Γ: D → C where C and D are FIX-categories. However, close inspection shows that it is not at all clear how to define a FPO in (C ↓ Γ), that is, there is certainly no obvious candidate for a FPO. In fact the author suspects that the comma category is not in general a FIX-category, though no counter example has been found. We shall provide a limited solution to this problem by giving a new gluing style construction in the case that C is a functor category with target ωCPO. This construction is most interesting in itself, but moreover will be put to good use in Section 7 where it provides a key step in the proof of a theorem.

For this section we proceed as follows. The first few propositions are devoted to showing that ωCPO^{C^{op}} is a FIX-category. We can then prove Theorem 6.7, a gluing construction, which is our main result. Finally, we prove a corollary which will be used crucially in Section 7.

Proposition 6.1 Let C be locally small. Then there is a NNO (N̂, ŝ, ˆ0) in the functor category ωCPO^{C^{op}}.

Proof A standard result for the topos Set^{C^{op}}. The same proof works here, namely, the NNO is defined pointwise. □

Proposition 6.2 Let C be locally small. Then the functor category ωCPO^{C^{op}} has finite products (for ωCPO does) and is in fact a let-category (⊥, η, lift) with a structure inherited from the lifting let-structure of ωCPO—see page 8.

Proof ωCPO^{C^{op}} is a let-category where

• if F: C^{op} → ωCPO then ⊥F sends an object C of C to (F C)_{⊥} and sends a morphism c: C′ → C in C to (F c)_{⊥},

• η_{F}: F → ⊥F is given by (η_{F})_{C} =^{def} ι_{F C}: F C → (F C)_{⊥}, and

• if α: F × F′ → F′′, then lift(α): F × ⊥F′ → F′′ is given by lift(α)_{C} =^{def} lift(α_{C}).

□

Proposition 6.3 There is a FPO (Ω̂, σ̂, ω̂) in ωCPO^{C^{op}} for the let structure (⊥, η, lift).

Proof We define Ω̂: C^{op} → ωCPO by sending an object C of C to the vertical natural numbers ℕ^{∞}, and any morphism of C^{op} to id_{ℕ^{∞}}. The natural transformations σ̂ and ω̂ are defined pointwise. □

Lemma 6.4 Let dis: Set → ωCPO map sets to discrete ωcpos, and write Y : C^{op} → Set^{C^{op}} for the Yoneda embedding. Write H =^{def} dis_{∗} ∘ Y : C^{op} → ωCPO^{C^{op}}.

Then ωCPO^{C^{op}} is an ωCPO enriched category and moreover there is an isomorphism

F C ≅ ωCPO^{C^{op}}(H_{C}, F)

in ωCPO which is natural in C and F.

Proof This is essentially the Yoneda lemma for enriched categories, but we give “bare hand” details.

Given objects (functors) F and F′ of the functor category ωCPO^{C^{op}}, we can regard the set of natural transformations ωCPO^{C^{op}}(F, F′) as a poset with the pointwise order, that is if α, α′: F → F′ then α ≤ α′ just in case for all objects C of ωCPO, α_{C} ≤ α′_{C} as Scott continuous functions (more precisely α_{C} ≤ α′_{C} in the exponential ωcpo F C ⇒ F′C).

It is easy to verify that ωCPO^{C^{op}}(F, F′) is an ωcpo: For let (α^{i} | i ∈ ω) be an ω-chain in ωCPO^{C^{op}}(F, F′). We need to see that the join of the chain exists. Clearly, if there is a natural transformation β: F → F′ whose component at an object A of C is β_{A} =^{def} ⨆_{i∈ω}α_{A}^{i} (and the latter join certainly exists) then ⨆_{i∈ω}α^{i} exists and is β. So let a: A′ → A in C and take any ξ ∈ F A; we need to see that

[figure: F A; β_{A}; F′A; F A′; F a; β_{A}; F′A′; F′a]

commutes. We have

F′a ∘ β_{A}(ξ) = F′a((⨆_{i∈ω}α_{A}^{i})ξ)
= F′a(⨆_{i∈ω}α_{A}^{i}(ξ))
= ⨆_{i∈ω}(F′a(α_{A}^{i}(ξ)))
= ⨆_{i∈ω}(α_{A′}^{i}(F a(ξ)))
= β_{A′} ∘ (F a)(ξ).

Thus ωCPO(F, F′) is an ωcpo and the functor category is certainly ωCPO-enriched. The required isomorphism in ωCPO follows by using the principle of the proof of the Yoneda lemma for Set. □

Proposition 6.5 The category ωCPO^{C^{op}} is a cartesian closed category with finite coproducts.

Proof Of course ωCPO has finite products implying that ωCPO^{C^{op}} does too from standard results. Let us look at cartesian closure. In fact the proof is essentially identical to that for the presheaf category Set^{C^{op}}.

Let F, F′: C^{op} → ωCPO be objects of the functor category. We define a functor F ⇒ F′: C^{op} → ωCPO as follows: on object C of C^{op} set

(F ⇒ F′)C =^{def} ωCPO^{C^{op}}(H_{C} × F, F′)

qua object of ωCPO via the enrichment of Lemma 6.4. Note that if the exponential F ⇒ F′ exists then it must have the above action on objects C by considering the bijection of Lemma 6.4. On morphisms c: C′ → C we define

(F ⇒ F′)c =^{def} ωCPO^{C^{op}}(H_{c} × id_{F} , id_{F′}).

It is routine to verify that (F ⇒ F′)c is a Scott continuous function.

We define a natural transformation ev: (F ⇒ F′) × F ⟶ F′ by giving a Scott continuous function ev_{C}: (F ⇒ F′)C × F C → F′C defined by ev_{C}(Φ, x) =^{def} Φ_{C}(id_{C}, x). Finally, if α: F × F′ → F′′ then λ(α): F → (F′ ⇒ F′′) is defined by giving for each object C of C a Scott continuous function

λ(α)_{C}: F C → (F′ ⇒ F′′)(C)

which is in turn defined by giving for each x ∈ F C and C′′ in C a Scott continuous function

λ(α)_{C}(x)_{C′} : C(C′, C) × F′C′ → F′′C′

given by λ(α)_{C}(x)_{C′}(c, x′) =^{def} α_{C′}(F (c)(x), x′). The detailed verification of continuity is routine. Once this is done the result follows from the standard proof that Set^{C^{op}} is cartesian closed. Finite coproducts are defined pointwise and we omit the details.

□

Corollary 6.6 ωCPO^{C^{op}} is a FIX-category.

Proof Follows from Propositions 6.1, 6.2, 6.3 and 6.5. □

We can now state and prove the most important result of this paper, which is a gluing style construction closely related to logical relations techniques. This theorem will be used to prove Corollary 6.8, and the corollary will be applied in Section 7.

Theorem 6.7 Let D be a FIX-category and let I: C → D preserve finite products. Write

Γ =^{def} (I^{op})^{∗} ∘ H: D ⟶ ωCPO^{D^{op}} ⟶ ωCPO^{C^{op}}.

We define a category Gl(Γ) as follows:

• The objects of Gl(Γ) are triples (F, ◁, D) where F: C^{op} → ωCPO is a functor, D is an object of D, and ◁ is an operation which assigns to each object C of C a subobject, denoted by ◁_{C}, of F C × ΓDC.

• A morphism (α, d): (F, ◁, D) → (F′, ◁′, D′) is given by a natural transformation α: F → F′ and a morphism d: D → D′ in D for which if x ◁_{C} u then α_{C}(x) ◁′_{C} d ∘ u, where of course x ∈ F C and u ∈ ΓDC =^{def} D(IC, D).

Then Gl(Γ) is a FIX-category (for a particular strong monad) and the obvious functor π_{2}: Gl(Γ) → D is a morphism of FIX-categories.

Proof That Gl(Γ) is indeed a category is routine. As a general principle, the structure of Gl(Γ) is specified by a “logical relations” procedure on the subobjects ◁_{C}. We sketch most of the constructions, giving full details for exponentials and the FPO; Corollary 6.6 is used implicitly.

(Terminal Object): The terminal object is (1_{ωCPO}_{C^{op}}, ◁^{1}, 1_{D}) where for an object C of C we set ∗ ◁_{C}^{1} !_{IC}. Here, ∗ ∈ 1_{ωCPO}_{C^{op}}(C) = {∗}, and !_{IC}: IC → 1_{D} is the unique map to the terminal object of D.

(Binary Products): We set

(F, ◁, D) × (F′, ◁′, D′) =^{def} (F × F′, ◁ × ◁′, D × D′)

where (x, x′)(◁ × ◁′)_{C}u just in case x ◁_{C} πu and x′ ◁′_{C} π′u where of course π: D × D′ → D and π′: D × D′ → D′ in D. It is easy to see that (◁ × ◁′)_{C} is indeed a subobject. The projections in Gl(Γ) are of course given by pairing of projections in ωCPO^{C^{op}} and D, such as:

π_{(F,◁,D)} =^{def} (π_{F} , π_{D}) : (F × F′, ◁ × ◁′, D × D′) ⟶ (F, ◁, D).

(Binary Coproducts): Write i: A → A + A′ and j: A′ → A + A′ for coproduct insertions.

We set

(F, ◁, D) + (F′, ◁′, D′) =^{def} (F + F′, ◁ + ◁′, D + D′)

where if x ∈ F C then i(x)(◁ + ◁′)_{C}u just in case u: IC → D + D′ factors through i: D → D + D′ in D and if x′ ∈ F′C then j(x′)(◁ + ◁′)_{C}u just in case u factors through j: D′ → D + D′ in D. (Note that every ξ ∈ F C + F′C is of the form i(x) or j(x′)).

(Exponentials): Set

(F, ◁, D) ⇒ (F′, ◁′, D′) =^{def} (F ⇒ F′, ◁⇒◁′, D ⇒ D′)

where Φ(◁⇒◁′)_{C}w just in case for all x ◁_{C} u we have

ev_{C}(Φ, x) ◁′_{C} ev ∘ ⟨w, u⟩

(ev_{C} was defined in the proof of Proposition 6.5). Let us check that (◁⇒◁′)_{C} is a subobject. Take a chain (Φ^{i}(◁⇒◁′)_{C}w | i ∈ ω) and let x ◁_{C} u. Then, using continuity of Φ_{C}^{i},

ev_{C}(⨆Φ^{i}, x) = (⨆Φ^{i})_{C}(id_{C}, x) = ⨆ev_{C}(Φ^{i}, x) ◁′_{C} ev ∘ ⟨w, u⟩

as required. The evaluation morphisms in Gl(Γ) are given pointwise, as is the operation of currying. So for example if (α, d) is a morphism in Gl(Γ) then we set λ((α, d)) =^{def} (λ(α), λ(d)): we check that this is a good definition. Suppose that x ◁_{C} u and x′ ◁′_{C} u′. Then

ev_{C}(λ(α)_{C}(x), x′) = α_{C}(x, x′) ◁′_{C} d ∘ ⟨u, u′⟩ = ev ∘ ⟨λ(d) ∘ u, u′⟩

and so λ(α)_{C}(x)(◁⇒◁′)_{C}λ(d) ∘ u whenever x ◁_{C} u.

(Strong Monad):

• T (F, ◁, D) =^{def} (⊥F, ◁^{T} , T D) where y ◁_{C}^{T} v just in case if y = [x] ∈ (F C)_{⊥} then v factors through η_{D} (by u say) and x ◁_{C} u.

• η_{(F,◁,d)} =^{def} (η_{F} , η_{D}).

• lift(α, d) =^{def} (lift(α), lift(d)), where, say,

(α, d) : (F, ◁, D) × T (F′, ◁′, D′) ⟶ T (F′′, ◁′′, D′′).

It is clear that we have indeed defined a strong monad provided that the definitions make sense. Let us verify that lift(α, d) is well defined. Suppose that

(x, y′)(◁ × ◁^{′T})_{C}t

and further that lift(α)_{C}(x, y′) = [x′′] ∈ (F′′C)_{⊥}. Then it remains to prove that lift(d) ∘ t factors through η_{D′′} (say by some ξ: IC → D′′) for which x′′ ◁′′_{C} ξ. Now we must have y′ = [x′] ∈ (F′C)_{⊥} and so [x′] ◁_{C}^{′T} π′t, implying π′t = η_{D′}u′ with x′ ◁′_{C} u′. But also x ◁_{C} πt and thus as (α, d) is a morphism in Gl(Γ) we have

[x′′] = α_{C}(x, x′) ◁_{C}^{′′T} d ∘ ⟨πt, u′⟩ = η_{D′′} ∘ ξ

for some ξ, where x′′ ◁′′_{C} ξ. Finally

lift(d) ∘ t = lift(d) ∘ (id × η_{D′}) ∘ ⟨πt, u′⟩ = d ∘ ⟨πt, u′⟩,

using LiftB.

(FPO): The FPO is (Ω̂, ◁, Ω) where ◁_{C} is a subobject of ℕ^{∞} ×D(IC, Ω) defined by

• ∞ ◁_{C} u just in case n ◁_{C}^{Ω} u for all n ∈ ℕ, and

• n ◁_{C}^{Ω} u if there is some u′: IC → T Ω for which u = (σ ∘ η_{Ω})^{n} ∘ σ ∘ u′.

The structure map is (σ̂, σ) and the global element is (ω̂, ω).

(NNO): The NNO is (N̂, ◁, N) where ◁_{C} is a subobject of ℕ × D(IC, N) given by n ◁ u iff u = s^{n} ∘ 0. The successor and zero morphisms are the expected ones.

It is easy to see that π_{2} is a FIX-category morphism. □

Corollary 6.8 Let C be a locally small category, and FC the freely generated FIX-category. Then the canonical functor I: C → FC is full and faithful.

Proof We appeal to Theorem 6.7 where D is taken to be FC. We define a functor J: C → Gl(Γ): on objects C of C define JC by (HC, ◁^{C}, IC) where the subobject

◁_{C′}^{C} ↪ C(C′, C) × D(IC′, IC)

is defined by requiring c ◁_{C′}^{C} Ic for each morphism c: C′ → C in C. Each ◁_{C′}^{C} is trivially a subobject, for

C(C′, C) × D(IC′, IC)

is a discrete ωcpo. On morphisms c of C we set Jc =^{def} (Hc, Ic). Note that J is faithful for the Yoneda embedding H is faithful. For fullness, let (α, d): JC → JC′. Hence α: HC → HC′ and so α = Hc for some c: C → C′ in C. Now certainly id_{C} ◁_{C}^{C} id_{IC} and so

α_{C}(id_{C}) = C(C, c)(id_{C}) = c ◁_{C}^{C′} d ∘ id_{IC} = d

implying d = I(c); therefore J(c) = (α, d), that is J is full.

The remainder of the proof follows by a diagram chasing argument identical to that of Corollary 5.2. □

Remark 6.9 In proving that I: C → FC is a full embedding, the crucial part of the proof is the construction of a category G (say) and a functor J: C → G which has particular factorisation properties. Theorem 5.1 is certainly a variant of Freyd’s original gluing construction. As we noted, the technique of Theorem 5.1 does not obviously carry over to categories with fixpoint objects. The new construction given in Theorem 6.7 works, of course, for let-cccs and in the author’s opinion furnishes a simpler construction of an appropriate glued category G than that of Theorem 5.1. The pointwise construction of exponentials in Gl(Γ) is much easier than the construction of exponentials in GL(Γ).

Remark 6.10 It is interesting to note the following: consider an instance of Γ, say the global sections Γ =^{def} D(1, −): D → Set, in Theorem 5.1. Take objects (X, f, D) and (X′, f′, D′) in GL(Γ), and recall that

(X, f, D) ⇒ (X′, f′, D′) =^{def} (P, p_{2}, D ⇒ D′)

arises from the pullback

(X ⇒ X′) ×_{X⇒ΓD′} Γ(D ⇒ D′) \overline{p_{2}  ^{}}Γ(D ⇒ D′)

[figure: X ⇒ X′; p_{1}; id ⇒ f′; X ⇒ ΓD′; λ(Γev∘ ≅ ∘(id × f))]

Take any θ ∈ X ⇒ X′ and λ(ϕ) ∈ Γ(D ⇒ D′) such that (θ, λ(ϕ)) ∈ P, and tracing the diagram we get

[figure: (θ, λ(ϕ)); λ(ϕ); θ; (x ↦ f′(θ(x)) = (x ↦ ϕ ∘ f(x))]

Now consider an analogue of Theorem 6.7 in which C =^{def} 1, the one point category, I =^{def} 1_{D}: 1 → D is the (obvious) constant functor, and we replace ωCPO by Set and H by Y . Identifying Set^{1} with Set, we have a category Gl(Γ). Now consider (X, f, D) and (X′, f′, D′) as objects of Gl(Γ) with exponential

(X ⇒ X′, f ⇒ f′, D ⇒ D′).

Certainly we have a subobject

(f ⇒ f′) ↪ (X ⇒ X′) × Γ(D ⇒ D′),

and it is easy to see that in fact (f ⇒ f′) = P, that is, the pullback construction of exponentials in GL(Γ) gives rise to exactly the logical relations style construction of exponentials in Gl(Γ).

7 A Conservative Extension via Full Embedding

We again assume that the reader is familiar with certain equational type theories. For details see [2] and [3].

Here, a FIX-theory^{6} Th = (Sg, Ax) is specified by giving a signature Sg of ground types γ and function symbols f: α_{1}, …, α_{n} → α_{n+1}, where the higher types are given by

α ::= γ | unit | fix | nat | α × α | α + α | α ⇒ α | T α,

and fix is the fixpoint type. Ax is a collection of equations-in-context Γ ⊢ M = M′: α giving the axioms of the theory. The theorems are generated by the usual β and η rules associated with the given types.

We aim to prove Theorem 7.1: very informally, we might say that “given an algebraic theory, the FIX-theory generated from it gives a more expressive syntax for programming, but does not increase the computational power of the original theory.” Note that for us, an algebraic theory is the type-theoretic counterpart of a category with finite products.

Theorem 7.1 Let Th = (Ax, Sg) be an algebraic theory where Sg is a signature of types and function symbols giving rise to well-formed terms-in-context (proved terms) of the form [x⃗: γ⃗] ⊢_{Sg} M: γ where [x⃗: γ⃗] is an environment of the form [x_{1}: γ_{1}, …, x_{n}: γ_{n}], M is a raw term, and Ax is a collection of equations-in-context of the form Γ ⊢ M = M′: γ. Write Th′ = (Ax′, Sg′) to indicate the FIX-theory which has the ground types the types of Sg, and axioms those of Ax. Then

(i) If [x⃗: γ⃗] ⊢_{Th}′ E: γ where γ_{i} and γ are ground types, then there is a raw term M of Sg such that

[x⃗: γ⃗] ⊢_{Sg} M: γ  and  [x⃗: γ⃗] ⊢_{Th}′ E = M: γ.

6A FIX-theory was called a FIX_{=}-theory in [4].

(ii) If also [x⃗: γ⃗] ⊢_{Th}′ E = M′: γ where [x⃗: γ⃗] ⊢_{Sg} M′: γ then

[x⃗: γ⃗] ⊢_{Th} M = M′: γ.

The key step in proving Theorem 7.1 is showing the following category-theoretic result:

Proposition 7.2 Let Th and Th′ be as in Theorem 7.1. Let us write Cl(Th) and Cl(Th′) for their respective classifying categories as an algebraic theory and a FIX-theory. Then Cl(Th′) is the freely generated FIX-category of Cl(Th) (via a functor I: Cl(Th) → Cl(Th′) to be given).

Proof This kind of result is prevalent in categorical type theory and the proof techniques routine. We sketch the details of the proof.

Objects of Cl(Th) are finite lists γ⃗ of types of Sg and a morphism

[([x⃗: γ⃗] | M_{1})_{Th}, …, ([x⃗: γ⃗] | M_{n})_{Th}]: γ⃗ ⟶ γ⃗′

is a list of equivalence classes of pairs ([x⃗: γ⃗], M) (where [x⃗: γ⃗] ⊢_{Sg} M_{i}: γ′_{i}) using the equivalence relation of provable equality in Th.

An object of Cl(Th′) is a type σ of Sg′, and a morphism (x: σ | M)_{Th}′: σ → τ is given by a similar equivalence class up to provable equality in Th′.

We define a finite product preserving functor I: Cl(Th) → Cl(Th′) by I(γ⃗) =^{def} Π_{1}^{n}γ_{i} and

I([([x⃗: γ⃗] | M_{1})_{Th}, …, ([x⃗: γ⃗] | M_{n})_{Th}]) =^{def} (z: Π_{1}^{n}γ_{i} | ⟨M̂_{1}, …, M̂_{n}⟩)_{Th}′

where M_{i} =^{def} M_{i}[Proj_{i}/x_{i}] and Proj_{i}(z) is the obvious raw term of the FIX-theory such that z: Π_{1}^{n}γ_{i} ⊢_{Sg} Proj_{i}(z): γ_{i}, and the sub-scripts Th and Th′ indicate in which theory we are taking provable equality.

Let F: Cl(Th) → D where D is a FIX-category. The definition of the functor \overline{F}: Cl(Th′) → D is by structural induction. We just give the cases involving T -types and the fix type.

• \overline{F} (T σ) =^{def} T (\overline{F} σ),

• \overline{F} (x: σ | Val(M)) =^{def} η_{\overline{F} τ} ∘ \overline{F} (x: σ | M), (where x: σ ⊢_{Sg} M: τ, say)

•

\overline{F} (x: σ | Let (E, y.F)) =^{def}

lift(\overline{F} (z: σ × τ | F [Fst(z), Snd(z)/x, y])) ∘ ⟨id_{\overline{F} σ}, \overline{F} (x: σ | E)⟩,

• \overline{F} (fix) =^{def} Ω for Ω in D, • \overline{F} (x: unit | ω) =^{def} ω in D,

• \overline{F} (x: σ | Inc(E)) =^{def} σ ∘ \overline{F} (x: σ | E),

•

\overline{F} (x: σ | It(y.F, N)) =^{def}

(\overline{F} (z: σ × T τ | F [Fst(z), Snd(z)/x, y])) ∘ ⟨id_{\overline{F}σ}, \overline{F} (x: σ | N )⟩.

It is immediate from its definition that \overline{F} is a FIX-category morphism.

We define a natural isomorphism ϕ: \overline{F} I → F: Cl(Th) → D by observing that at each object γ⃗ of Cl(Th) we have

\overline{F} I(γ⃗) = \overline{F} (Π_{1}^{n}γ_{i}) =^{def} Π_{1}^{n}F ([γ_{i}]) ≅ F (γ⃗)

in D. One can prove by a lengthy structural induction over the morphisms of Cl(Th) that the above isomorphisms give rise to a natural isomorphism ϕ. □

Now we can prove Theorem 7.1:

Proof It follows from Corollary 6.8 that I: Cl(Th) → Cl(Th′) is a full embedding, and this proves the theorem: we expand on the details for the existence part of the theorem. Suppose that x_{1}: γ_{1}, …, x_{n}: γ_{n} ⊢_{Sg}′ E: γ. We shall write

Ê =^{def} E[Proj_{1}(z)/x_{1}, …, Proj_{j}(z)/x_{j}, …, Proj_{n}(z)/x_{n}]

and

Πγ⃗ =^{def} (… (γ_{1} × γ_{2}) × …) × γ_{n}.

Then we certainly have e =^{def} (z: Πγ⃗ | Ê)_{Th}′: Iγ⃗ → I[γ] in E′. Using the fullness of I, there is a morphism ([x_{1}: γ_{1}, …, x_{n}: γ_{n}] | M)_{Th}: γ⃗ → [γ] which is taken to e by I. But this implies that z: Πγ⃗ ⊢_{Th}′ M̂ = Ê: γ (using an obvious notation for M̂) and so x_{1}: γ_{1}, …, x_{n}: γ_{n} ⊢_{Th}′ M = E: γ. The uniqueness part of the theorem follows from I’s faithfulness in a similar fashion. □

Remark 7.3 The original (category-theoretic) proof that “λ-calculus is conservative over algebra” uses techniques similar to those found in Theorem 5.1 and Corollary 5.2. We have included these two results for their intrinsic interest, and because they amount to the obvious extension of the original proof technique. However, for the purposes of proving the results in Section 7, the methods of Section 6 subsume those of Section 5.

8 Conclusions and Acknowledgements

We have presented some miscellaneous results about fixpoint objects. We have also extended some standard ideas of category theory, such as polynomial categories and gluing (for cccs), to cccs equipped with a strong monad. We noted that the usual gluing construction does not obviously apply to FIX-categories, and solved the problem by giving a new, but similar, construction for a limited class of functors. This yields a corresponding type-theoretic conservative extension result for FIXtheories.

The precise relationship between the underlying construction of Gl(Γ), and the logical-relations structure of GL(Γ) needs to be understood from a more abstract point of view. The form of the construction of the latter category also needs to be compared with other applications of gluing, such as the existence and disjunction properties of intuitionistic logic.

I would like to thank Martin Hyland and Andrew Pitts for comments on material in Sections 2 to 5. Thanks to the U.K. Engineering and Physical Sciences Research Council (formally SERC) for funding in the form of a Research Fellowship. Two referees supplied a number of astute comments on the original version of this paper, which I have acted upon. I believe that their reports have significantly improved the original presentation, and also resulted in non-trivial changes and additions to a couple of proofs. I am most grateful to them for their advice. Last, but not least, the commutative diagrams were drawn using Paul Taylor’s Commutative Diagrams package.

References

[1] M. Barr and C. Wells.: 1990, Category Theory for Computing Science, International Series in Computer Science, Prentice Hall.

[2] Crole R.L.: 1993, Categories for Types, Cambridge Mathematical Textbooks, Cambridge University Press.

[3] Crole R. L.:1991, Programming Metalogics with a Fixpoint Type, PhD thesis, Computer Laboratory, University of Cambridge.

[4] Crole R. L. and Pitts A. M.:1992, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, Information and Computation,Vol. no. 98 pp. 171–210.

[5] Freyd P. J. and Scedrov A.: 1990, Categories, Allegories, North Holland.

[6] Semantics of Programming Languages: Structures and Techniques: 1992, Foundations of Computing, MIT Press.

[7] Jacobs B.:1991, Categorical Type Theory. Ph.D. thesis, University of Nijmegen.

[8] Johnstone P. T.:1977, Topos Theory, Academic Press.

[9] Kock A.:1970, Monads on symmetric monoidal closed categories, Archiv der Mathematik,Vol. no. 21, pp. 1–10.

[10] Lafont Y.:1988, Logiques, Catégories et Machines, PhD thesis, Univ. Paris VII.

[11] Lambek J. and Scott P. J.:1980, Intuitionist type theory and the free topos, Journal of Pure and Applied Algebra,Vol. no. 19, pp. 215–257.

[12] Lambek J. and Scott P. J.:1986, Introduction to Higher Order Categorical Logic, Cambridge Studies in Advanced Mathematics, Cambridge University Press.

[13] Mac Lane S.:1971, Categories for the Working Mathematician, Graduate Texts in Mathematics, Springer-Verlag, Vol. no. 5.

[14] Moggi E.:1989, Notions of computation and monads, Theoretical Computer Science, Vol. no. 93, pp. 55–92.

[15] Pitts A. M.:1995, Categorical Logic. To appear in the Handbook of Logic in Computer Science, Abramsky S., Gabbay, D. M. and Maibaum T. S. E. (eds), Oxford University Press. Technical Report No. 367, University of Cambridge Computer Laboratory,

[16] Plotkin G.D.:1981, Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”), Dept. of Computer Science, Univ. of Edinburgh.