Theory and Applications of Categories, Vol. 20, No. 1, 2008, pp. 5–17.

LOCALLY CARTESIAN CLOSED CATEGORIES WITHOUT CHOSEN CONSTRUCTIONS

ERIK PALMGREN

Abstract. We show how to formulate the notion of locally cartesian closed category without chosen pullbacks, by the use of Makkai’s theory of anafunctors.

1. Introduction

The standard formulation of a locally cartesian closed category (LCCC) depends on the assumption of chosen pullbacks. One may not always assume that such pullbacks can be chosen, working inside a topos, or in a meta-theory which lacks the full axiom of choice. Such theories are, for instance, Zermelo-Fraenkel set theory, ZF, or constructive theories of types and sets. Makkai [2, 3] developed a theory of generalised functors, anafunctors, which can handle non-chosen limit constructions in a functorial way. We shall here apply this theory to the example of LCCC. We thus give a formulation of LCCCs without chosen constructions. In the course of this we also note that some basic results about adjoints carry over to the anafunctor setting (Theorems 2.3 and 3.2). The results in Sections 4 and 5 indicate that categorical logic may be developed smoothly without chosen constructions.

2. Anafunctors

We choose to use the “span formulation” of anafunctors given in [2]. Let X and A be categories. An anafunctor F from X to A is a category |F | and pair of functors

F_{0} : |F |  [figure] X and F_{1} : |F |  [figure] A such that F_{0} satisfies the conditions

(A1) F_{0} is surjective on objects,

(A2) for any s, t ∈ |F | and g : F_{0}(s)  [figure] F_{0}(t) there is a unique f : s  [figure] t with g = F_{0}(f).

Denote this f by |g|_{s,t}.

The author is supported by a grant from the Swedish Research Council (VR).

Received by the editors 2006-12-20 and, in revised form, 2007-09-03.

Transmitted by Richard Blute. Published on 2008-01-14.

2000 Mathematics Subject Classification: 18A35, 18A40.

Key words and phrases: anafunctor, axiom of choice, adjoint.

\begin{matrix}c \\ ◯ \end{matrix} Erik Palmgren, 2008. Permission to copy for private use granted.

We write F : X [figure] A for such an anafunctor. In short, it is thus a span of ordinary functors

[figure: X; A; |F |; X; F_{0}; |F |; A; F_{1}]

where F_{0} is full, faithful and surjective on objects.

Note that for s, t ∈ |F | with X = F_{0}(s) = F_{0}(t) the morphism |id_{X}|_{s,t} : s [figure] t is an isomorphism. For s = t, |id_{X}|_{s,t} is id_{s}. Note, further, that if X ⟶^{f} Y ⟶^{g} Z in X, then for any r, s, t ∈ |F | with F_{0}(r) = X, F_{0}(s) = Y, F_{0}(t) = Z, we have |g ∘f|_{r,t} = |g|_{s,t} ∘|f|_{r,s}.

A standard functor F : X [figure] A becomes an anafunctor F̂ : X [figure] A by letting |F̂| = X, F̂_{1} = F and letting F̂_{0} be the identity functor on X.

2.1. Remark. Using the axiom of choice, we may, given an anafunctor G : X [figure] A, construct a standard functor Ǧ : X [figure] A as follows. For any object X of X choose H(X) in |G| with G_{0}(H(X)) = X. Then put Ǧ(X) = G_{1}(H(X)) and, for f : X [figure] Y, let Ǧ(f) = G_{1}(|f|_{H(X),H(Y)}).

2.2. Remark. The composition of anafunctors is a composition of spans using a pullback, and is associative merely up to canonical isomorphism. In [2] it is shown that categories, anafunctors and natural transformations form a (super large) bicategory.

An anafunctor F : X [figure] A is said to preserve colimits of type I if, and only if, for every functor H : I [figure] |F | and c ∈ |F |, τ : H [figure: .]Δ(c): whenever F_{0}τ : F_{0}H [figure: .]F_{0}Δ(c) is a colimiting cone then so is F_{1}τ : F_{1}H [figure: .]F_{1}Δ(c). Preservation of limits is defined dually. An anafunctor F : X [figure] A is said to preserve property P of arrows, if for any f : s [figure] t in |F |, whenever F_{0}(f) has property P, then so has F_{1}(f). Let F : X [figure] A and G : A[figure] X be anafunctors. Then F is left adjoint (or anaadjoint) to G if for t ∈ |F | and v ∈ |G| there are bijections

φ_{t,v} : A(F_{1}(t), G_{0}(v))  [figure] X (F_{0}(t), G_{1}(v))  (1)

satisfying the following naturality conditions

(N1) for s, t ∈ |F |, v ∈ |G|, h : s [figure] t, f ∈ A(F_{1}(t), G_{0}(v))

φ_{t,v}(f) ∘ F_{0}(h) = φ_{s,v}(f ∘ F_{1}(h))

(N2) for t ∈ |F |, v, w ∈ |G|, k : v [figure] w, g ∈ X (F_{0}(t), G_{1}(v))

G_{0}(k) ∘ φ_{t,v}^{−1}(g) = φ_{t,w}^{−1}(G_{1}(k) ∘ g).

Note a particular case of (N1) where h : s [figure] t is such that F_{0}(h) = id_{X} where X = F_{0}(s) = F_{0}(t). Then φ_{t,v}(f) = φ_{s,v}(f ∘ F_{1}(h)) and F_{1}(h) is an isomorphism.

We have as for usual adjoints, and with a similar proof:

LOCALLY CARTESIAN CLOSED CATEGORIES WITHOUT CHOSEN CONSTRUCTIONS 7

2.3. Theorem. Let F : X [figure] A and G : A [figure] X be anafunctors such that F is left adjoint to G. Then:

(i) F preserves colimits of any type,

(ii) F preserves epis,

(iii) G preserves limits of any type,

(iv) G preserves monos.

2.4. Example. Suppose that F : X [figure] A is left adjoint to G : A [figure] X. For diagrams of finite type, i.e. where I is a finite category such as indicated by

[figure: •; •; •; •; •; •; •]  (2)

The axiom of choice is not needed for a finite category and we can reason as follows. Suppose that

X [figure: f; g] Y [figure: q] Z

is a coequalizer diagram in X. Pick some r, s, t ∈ |F | with F_{0}(r) = X, F_{0}(s) = Y and F_{0}(t) = Z using (A1). Now, since F preserves colimits of the type to the right in (2), the following is a coequalizer diagram in A

F_{1}(r) [figure: F_{1}(|f|_{r,s}); F_{1}(|g|_{r,s})] F_{1}(s) [figure: F_{1}(|q|_{s,t})] F_{1}(t)

This holds regardless of the choices of r, s, t satisfying the above equations.

For later reference we give details of the constructions involved in proofs (see [2]) of the equivalence between local and global existence conditions for anaadjoints. This is a generalisation of the corresponding results for ordinary functors [1]. An anafunctor F : X [figure] A satisfies the local existence condition for a right adjoint (LR) if for any A ∈ A there are s ∈ |F |, ε : F_{1}(s) [figure] A such that

(*) for each t ∈ |F | and each h : F_{1}(t)  [figure] A there is a unique ĥ : t  [figure] s with

ε ∘ F_{1}(ĥ) = h.

2.5. Lemma. An anafunctor F : X [figure] A satisfies (LR) if, and only if, there is a right adjoint G : A [figure] X to F.

Proof. ( [figure] ) Suppose that G : A [figure] X is right adjoint to F and that φ_{t,v} is a family of bijections witnessing the adjunction as in (1). We verify (LR): Let A ∈ A be given. Then take v ∈ |G| with A = G_{0}(v) and then s ∈ |F | with F_{0}(s) = G_{1}(v). Put

ε = φ_{s,v}^{−1}(id_{G_{1}(v)}) : F_{1}(s)  [figure] A.  (3)

Now consider any t ∈ |F | and h : F_{1}(t) [figure] A. Then k = φ_{t,v}(h) : F_{0}(t) [figure] G_{1}(v) = F_{0}(s). Let ĥ = |k|_{t,s} : t [figure] s. Hence by (N1) and inverting φ_{t,v}

ε ∘ F_{1}(ĥ) = φ_{s,v}^{−1}(id_{G_{1}(v)} ∘ F_{1}(ĥ))
= φ_{t,v}^{−1}(φ_{s,v}(φ_{s,v}^{−1}(id_{G_{1}(v)}) ∘ F_{0}(ĥ))
= φ_{t,v}^{−1}(id_{G_{1}(v)} ∘ F_{0}(ĥ))
= φ_{t,v}^{−1}(F_{0}(ĥ)) = φ_{t,v}^{−1}(k) = h.

Suppose that h′ : t [figure] s satisfies ε ∘ F_{1}(h′) = h. As above ε ∘ F_{1}(ĥ) = φ_{t,v}^{−1}(F_{0}(h′)). Thus φ_{t,v}^{−1}(F_{0}(h′)) = φ_{t,v}^{−1}(F_{0}(ĥ)), and since φ_{t,v} is a bijection F_{0}(h′) = F_{0}(ĥ). As F_{0} is faithful, we have in fact h′ = ĥ.

For h′ : t [figure] s we note a useful identity

ε ∘ F_{1}(h′) = φ_{t,v}^{−1}(F_{0}(h′)).  (4)

( [figure] ) We construct G as follows. Let |G| be the category whose objects are triples (A, s, ε) where A ∈ A, s ∈ |F |, ε : F_{1}(s) [figure] A satisfies universal property (*). In this category a morphism from (A, s, ε) to (A′, s′, ε′) is a pair (f, g) where f : s [figure] s′, g : A [figure] A′ are such that the square

[figure: F_{1}(s′); A′; ε′; F_{1}(s); F_{1}(s′); F_{1}(f); F_{1}(s); A; ε; A; A′; g]

commutes. According to the universal property of (A′, s′, ε′) the morphism f is determined uniquely by g. Next, define G_{0} : |G| [figure] A by G_{0}(A, s, ε) = A and G_{0}(f, g) = g, which is seen to be a functor that satisfies (A2). By (LR) it follows that (A1) holds. Then define G_{1} : |G| [figure] X by G_{1}(A, s, ε) = F_{0}(s) and G_{1}(f, g) = F_{0}(f). Thus G : A [figure] X is an anafunctor. To prove that F is left adjoint to G we construct, for t ∈ |F | and v = (A, p, ε) ∈ |G|, the bijection

φ_{t,v} : A(F_{1}(t), G_{0}(v)) [figure] X (F_{0}(t), G_{1}(v))

as follows. We have ε : F_{1}(p) [figure] A and A = G_{0}(p) since v ∈ |G|. For any h ∈ A(F_{1}(t), G_{0}(v)) there is a unique ĥ : t [figure] p with ε ∘ F_{1}(ĥ) = h. Let φ_{t,v}(h) = F_{0}(ĥ).

Now if φ_{t,v}(h_{2}) = φ_{t,v}(h), then by faithfulness of F_{0} we get ĥ = ĥ_{2}. Therefore h = h_{2} as well. For a given k ∈ X (F_{0}(t), G_{1}(v)), we have for some h : t [figure] p that F_{0}(h) = k , as G_{1}(v) = F_{0}(p). Thus trivially φ_{t,u}(ε ∘ F_{1}(h)) = k.

To verify the naturality conditions (N1) and (N2) is straightforward.

Dually we have the following notion. An anafunctor G : A [figure] X satisfies the local existence condition for a left adjoint (LL) if for any X ∈ X there is s ∈ |G| and η : X [figure] G_{1}(s) such that

(**) for each t ∈ |G| and each f : X  [figure] G_{1}(t) there is a unique f̂ : s  [figure] t with

G_{1}(f̂) ∘ η = f.

2.6. Lemma. An anafunctor G : A [figure] X satisfies (LL) if, and only if, there is a left adjoint F : X [figure] A to G.

Proof. The anafunctor F is constructed as follows. It is analogous to that of Lemma 2.5, but we spell it out for completeness. The proof of its properties is omitted., being dual to that of the mentioned lemma.

The category |F | consists of triples (X, s, η) satisfying property (**). A morphism (f, g) : (X, s, η) [figure] (X′, s′, η′) consists of f : X [figure] X′ and g : s [figure] s′ such that the square

[figure: X′; G_{1}(s′); η′; X; X′; f; X; G_{1}(s); η; G_{1}(s); G_{1}(s′); G_{1}(g)]

commutes. According to the universal property, g is determined uniquely by f.

Define F_{0} : |F | [figure]X and F_{1} : |F | [figure]A by F_{0}(X, s, η) = X, F_{0}(f, g) = f, F_{1}(X, s, η) = G_{0}(s) and F_{1}(f, g) = g. By the (LL) property it follows that F is an anafunctor.

3. Natural transformations

We recall the definition from [2]. A natural transformation h : F [figure] G between two anafunctors F, G : X [figure] A is a family h_{s,t} : F_{1}(s) [figure] G_{1}(t) (s ∈ |F |, t ∈ |G|, F_{0}(s) = G_{0}(t)) of morphisms in A such that for all f : s [figure] u and g : t [figure] v, with F_{0}(s) = G_{0}(t), F_{0}(u) = G_{0}(v) and F_{0}(f) = G_{0}(g), the diagram

[figure: G_{1}(t); G_{1}(v); G_{1}(g); F_{1}(s); G_{1}(t); h_{s,t}; F_{1}(s); F_{1}(u); F_{1}(f); F_{1}(u); G_{1}(v); h_{u,v}]

commutes. In case F and G are ordinary functors, i.e. F_{0} = G_{0} = Id_{X}, this reduces to the standard notion of natural transformation.

We now prove a little coherence result. Suppose that k : G [figure] H is another natural transformation, where G, H : X [figure] A are anafunctors. Then we claim that the diagram

[figure: G_{1}(t); H_{1}(r); k_{t,r}; F_{1}(s); G_{1}(t); h_{s,t}; F_{1}(s); G_{1}(t′); h_{s,t′}; G_{1}(t′); H_{1}(r); k_{t′,r}]

commutes for any s ∈ |F |, t, t′ ∈ |G|, r ∈ |H| with X = F_{0}(s) = G_{0}(t) = G_{0}(t′) = H_{0}(r). There is a unique g : t [figure] t′ with G_{0}(g) = id_{X}. Then F_{0}(id_{s}) = H_{0}(id_{t}) = G_{0}(g), so by naturality we have

k_{t′,r} ∘ h_{s,t′} = k_{t′,r} ∘ h_{s,t′} ∘ F_{1}(id_{s})
= k_{t′,r} ∘ G_{1}(g) ∘ h_{s,t}
= H_{1}(id_{r}) ∘ k_{t,r} ∘ h_{s,t}
= k_{t,r} ∘ h_{s,t}

Thus define the composition of k and h by

(k · h)_{s,r} = k_{t,r} ∘ h_{s,t}

where t is any element of |G| with F_{0}(s) = G_{0}(t) = H_{0}(r). Such t exists since G is surjective on objects. It follows that (k · h)_{s,r} is well-defined. Naturality is clear by the naturality of h and k.

For an anafunctor F : X [figure] A the identity natural transformation 1_{F} : F [figure] F is defined by (1_{F})_{s,t} = F_{1}(|id_{X}|_{s,t}) for s, t ∈ |F | with X = F_{0}(s) = F_{0}(t). A natural transformation h : F [figure] G between two anafunctors F, G : X [figure] A is a natural isomorphism if there is a natural transformation k : G [figure] F such that k · h = 1_{F} and h · k = 1_{G}. We omit the straightforward verification of the following lemma.

3.1. Lemma. Let F, G : X [figure] A be anafunctors, and let h : F [figure] G be a natural transformation. Then h is a natural isomorphism if, and only if, h_{s,t} : F_{1}(s) [figure] G_{1}(t) is an isomorphism for all s ∈ |F |, t ∈ |G| with F_{0}(s) = G_{0}(t).

It is now possible to generalise the uniqueness results for adjoints to the anafunctor case.

3.2. Theorem. Left and right adjoints (if they exist) of an anafunctor F : X [figure] A are unique up to natural isomorphism.

Proof. We prove this for right adjoints. Suppose that G, G′ : A [figure] X are both right adjoints of F. Thus there are families of bijections

φ_{t,v} : A(F_{1}(t), G_{0}(v)) [figure] X (F_{0}(t), G_{1}(v)) (t ∈ |F |, v ∈ |G|)

and

φ′_{t,v′} : A(F_{1}(t), G′_{0}(v′)) [figure] X (F_{0}(t), G′_{1}(v)) (t ∈ |F |, v′ ∈ |G′|)

satisfying (N1) and (N2).

We construct h_{v,v′} : G_{1}(v) [figure] G′_{1}(v′) for v ∈ |G| and v′ ∈ |G′| with G_{0}(v) = G′_{0}(v′). Take s, s′ ∈ |F | with F_{0}(s) = G_{1}(v) and F_{0}(s′) = G′_{1}(v′) and consider the counits

ε_{s,v} = φ_{s,v}^{−1}(id_{G_{1}(v)}) : F_{1}(s)  [figure] G_{0}(v)
ε′_{s′,v′} = φ′_{s′,v′}^{−1}(id_{G′_{1}(v′)}) : F_{1}(s′)  [figure] G′_{0}(v′).

Since G_{0}(v) = G′_{0}(v′), there is thus a unique f : s [figure] s′ with ε′_{s′,v′} ∘ F_{1}(f) = ε_{s,v} and a unique g : s′ [figure] s with ε_{s,v} ∘ F_{1}(g) = ε′_{s′,v′}. It follows by the universal properties that g is the inverse to f. Write θ_{s,s′,v,v′} = f. Define

h_{v,v′} = F_{0}(θ_{s,s′,v,v′}).

This is an iso. We need to show that this definition does not depend on s and s′. Suppose t, t′ ∈ |F | with F_{0}(t) = G_{1}(v) and F_{0}(t′) = G′_{1}(v′). There are unique k : s [figure] t and k′ : s′ [figure] t′ with F_{0}(k) = id_{G_{1}(v)} and F_{0}(k′) = id_{G′_{1}(v′)}. Thus to show F_{0}(θ_{s,s′,v,v′}) = F_{0}(θ_{t,t′,v,v′}) it suffices to prove

k′ ∘ θ_{s,s′,v,v′} = θ_{t,t′,v,v′} ∘ k.

This is done by verifying that

ε′_{t′,v′} ∘ F_{1}(k′ ∘ θ_{s,s′,v,v′}) = ε′_{t′,v′} ∘ F_{1}(θ_{t,t′,v,v′} ∘ k)

from which the identity follows by the uniqueness. Indeed, we have using (N1) in the second step and properties of the units of the adjunction

ε′_{t′,v′} ∘ F_{1}(k′ ∘ θ_{s,s′,v,v′}) = φ′_{t′,v′}^{−1}(id_{G′_{1}(v′)}) ∘ F_{1}(k′) ∘ F_{1}(θ_{s,s′,v,v′})
= φ′_{s′,v′}^{−1}(φ′_{t′,v′}(φ′_{t′,v′}^{−1}(id_{G′_{1}(v′)})) ∘ F_{0}(k′)) ∘ F_{1}(θ_{s,s′,v,v′})
= φ′_{s′,v′}^{−1}(id_{G′_{1}(v′)} ∘ id_{G′_{1}(v′)}) ∘ F_{1}(θ_{s,s′,v,v′})
= ε′_{s′,v′} ∘ F_{1}(θ_{s,s′,v,v′})
= ε_{s,v}
= φ_{s,v}^{−1}(id_{G_{1}(v)})
= φ_{s,v}^{−1}(φ_{t,v}(φ_{t,v}^{−1}(id_{G_{1}(v)})) ∘ F_{0}(k))
= φ_{t,v}^{−1}(id_{G_{1}(v)}) ∘ F_{1}(k)
= ε_{t,v} ∘ F_{1}(k)
= ε′_{t′,v′} ∘ F_{1}(θ_{t,t′,v,v′}) ∘ F_{1}(k)
= ε′_{t′,v′} ∘ F_{1}(θ_{t,t′,v,v′} ∘ k).

Thus h_{v,w} is well-defined and iso. We finally verify that these morphisms form a natural transformation. Consider α : v [figure] w and α′ : v′ [figure] w′ with G_{0}(v) = G′_{0}(v′), G_{0}(w) = G′_{0}(w′) and G_{0}(α) = G′_{0}(α′). We show that

[figure: G_{1}(w); G′_{1}(w′); h_{w,w′}; G_{1}(v); G_{1}(w); G_{1}(α); G_{1}(v); G′_{1}(v′); h_{v,v′}; G′_{1}(v′); G′_{1}(w′); G′_{1}(α′)]

commutes. We consider some s, s′, t, t′ with F_{0}(s) = G_{1}(v), F_{0}(s′) = G′_{1}(v′), F_{0}(t) = G_{1}(w), F_{0}(t′) = G′_{1}(w′). Then

h_{v,v′} = F_{0}(θ_{s,s′,v,v′}) h_{w,w′} = F_{0}(θ_{t,t′,w,w′}).

There are unique a : s  [figure] t and a′ : s′  [figure] t′ with F_{0}(a) = G_{1}(α) and F_{0}(a′) = G′_{1}(α′).

It is sufficient to check

θ_{t,t′,w,w′} ∘ a = a′ ∘ θ_{s,s′,v,v′} : s [figure] t′.

As above we get the first step of

ε′_{t′,w′} ∘ F_{1}(a′ ∘ θ_{s,s′,v,v′}) = φ′_{s′,w′}^{−1}(φ′_{t′,w′}(φ′_{t′,w′}^{−1}(id_{G′_{1}(w′)}) ∘ F_{0}(a′)) ∘ F_{1}(θ_{s,s′,v,v′})
= φ′_{s′,w′}^{−1}(F_{0}(a′)) ∘ F_{1}(θ_{s,s′,v,v′})
= φ′_{s′,w′}^{−1}(G′_{1}(α′)) ∘ F_{1}(θ_{s,s′,v,v′})
= G′_{0}(α′) ∘ φ′_{s′,v′}^{−1}(id_{G′_{1}(v′)}) ∘ F_{1}(θ_{s,s′,v,v′}) (using N2)
= G′_{0}(α′) ∘ ε′_{s′,v′} ∘ F_{1}(θ_{s,s′,v,v′})
= G′_{0}(α′) ∘ ε_{s,v}
= G_{0}(α) ∘ ε_{s,v}
= G_{0}(α) ∘ φ_{s,v}^{−1}(id_{G_{1}(v)})
= φ_{s,w}^{−1}(F_{0}(α))  (using N2)
= ε_{t,w} ∘ F_{1}(a)  (by (4))
= ε′_{t′,w′} ∘ F_{1}(θ_{t,t′,w,w′}) ∘ F_{1}(a)
= ε′_{t′,w′} ∘ F_{1}(θ_{t,t′,w,w′} ∘ a)

This proves that h forms a natural transformation.

4. Locally cartesian closed categories

Convention.. The objects of a slice category C/X are morphisms a : A [figure] X, and will be written (A, a). As a further abbreviation we write α = (A, a), β = (B, b), γ = (C, c) etc.

For any morphism f : X  [figure] Y the functor Σ_{f} : C/X  [figure] C/Y is given by composition

with f on objects, Σ_{f}(α) = (A, f ∘a), and defined as the identity on morphisms Σ_{f}(h) = h. We regard this functor as an anafunctor S = S_{f} : C/X [figure] C/Y, so |S| = C/X, S_{0} = Id_{|S|} and S_{1} = Σ_{f}. The (LR) condition for S now says: for any α ∈ C/Y there is some π ∈ C/X and e : (P, f ∘ p) [figure] α such that for each π′ ∈ C/X and each h : (P′, f ∘ p′) [figure] α there is a unique ĥ : π′ [figure] π with e ∘ ĥ = h. This says, in other words, that for any α ∈ C/Y there are morphisms p and e such that the following diagram is a pullback

[figure: X; Y; f; P; X; p; P; A; e; A; Y; a]

Suppose that C is a category where pullbacks exists (but are not necessarily chosen). The following can now be obtained from the construction in Lemma 2.5. Define for f : X [figure] Y an anafunctor F_{f} = F : C/Y [figure] C/X that expresses pullback along f. The category |F | consists of objects (β, π, q) where β ∈ C/Y, π ∈ C/X and where

[figure: X; Y; f; P; X; p; P; B; q; B; Y; b]

is a pullback square. A morphism (h, k) : (β, π, q) [figure] (β′, π′, q′) consists of morphisms

h : π  [figure] π′ and k : β  [figure] β′ in C/X and C/Y respectively, such that

[figure: P′; B′; q′; P; P′; h; P; B; q; B; B′; k]

commutes. Define functors F_{0} : |F | [figure] C/Y by F_{0}(β, π, q) = β and F_{0}(h, k) = k and F_{1} : |F | [figure] C/X by F_{1}(β, π, q) = π and F_{1}(h, k) = h. The functor F_{0} is surjective on objects since pullbacks exists. As for (A2) suppose k : F_{0}(β, π, q) [figure] F_{0}(β′, π′, q′), i.e. k : β [figure] β′. By the pullback property, there is a unique map h : P [figure] P′ with p′h = p and kq = q′h, i.e. such that (h, k) : (β, π, q) [figure] (β′, π′, q′) is a morphism. This shows (A2). Hence we have shown:

4.1. Lemma. Let C be a category with pullbacks. For any f : X [figure] Y the anafunctor S_{f} : C/X [figure] C/Y is left adjoint to F_{f} : C/Y [figure] C/X.

We shall employ the usual notations Σ_{f} and f^{∗} for anafunctors S_{f} and F_{f} respectively. The next step is to spell out the condition for f^{∗} to have a right anaadjoint. This gives a functorial definition of LCCCs without chosen constructions. The (LR) condition for F = f^{∗} : C/Y [figure] C/X becomes explicitly: for every γ ∈ C/X there are (***) s = (β, π, q) ∈ |F | and e : F_{1}(s) = π [figure] γ in C/X, i.e. there is a commutative diagram

[figure: C; e; C; c; X; Y; f; P; X; p; P; B; q; B; Y; b]  (5)

which is such that, if there is any other commutative diagram

[figure: C; h; C; c; X; Y; f; P′; X; p′; P′; B′; q′; B′; Y; b′]  (6)

i.e. t = (β′, π′, q′) ∈ |F | and h : F_{1}(t) = π′  [figure] γ then there is a unique (m, n) : t  [figure] s

such that

e ∘ m = h.  (7)

Note that m is determined by n : β′ [figure] β because of the pullback property.

For any category C, let Mon_{C}(X) be the full subcategory of C/X determined by objects that are monomorphisms going into X.

4.2. Lemma. Let C be a category with pullbacks. Let f : X [figure] Y be a morphism in C. If f^{∗} : C/Y [figure] C/X satisfies the (LR) condition, then the anafunctor Π_{f} : C/X [figure] C/Y, constructed as follows, is a right adjoint to f^{∗}. The category |Π_{f}| consists of triples (γ, s, e) such that (***) above is satisfied. Moreover, for s = (β, π, q) and ((h, k), ℓ) : (γ, s, e) [figure] (γ′, s′, e′),

(Π_{f})_{0}(γ, s, e) = γ
(Π_{f})_{0}((h, k), ℓ) = ℓ
(Π_{f})_{1}(γ, s, e) = (f^{∗})_{0}(s) = β
(Π_{f})_{1}((h, k), ℓ) = (f^{∗})_{0}(h, k) = k.

Moreover, the functor Π_{f} restricts to an anafunctor Mon_{C}(X) [figure] Mon_{C}(Y).

Proof. The first part follows directly from the general construction of a right adjoint in Lemma 2.5.

As for the second part, let (γ, s, e) ∈ |Π_{f}| and s = (β, π, q) and suppose that γ ∈ Mon_{C}(X), i.e. c : C [figure] X is mono. We show that b : B [figure] Y is mono. Let r_{1}, r_{2} : B′ [figure] B be so that br_{1} = br_{2}. Let b′ = br_{1}. Form the pullback

[figure: X; Y; f; P′; X; p′; P′; B′; q′; B′; Y; b′]

As b′ = br_{1} = br_{2} there is, for each k = 1, 2, a unique u_{k} : P′ [figure] P with qu_{k} = r_{k}q′ and pu_{k} = p′. By the equality pu_{1} = pu_{2} we get ceu_{1} = ceu_{2}. Thus, since c is mono, eu_{1} = eu_{2}. Let h = eu_{1}. Hence ch = ceu_{1} = pu_{1} = p′. Thus we have a diagram just as (6), with t = (π′, β′, q′). Let (m, n) : t [figure] s be the unique morphism such that e ∘ m = h. By the above (m, n) = (u_{k}, r_{k}), k = 1, 2, also satisfies these conditions. Hence r_{1} = r_{2}, which proves b to be mono.

5. Images and order reflection

Though images of morphisms may be formulated straightforwardly without any chosen construct, we show how they arise by a left anaadjoint of the inclusion functor.

For any category C and any object X of the category, let Inc_{X} : Mon_{C}(X) [figure] C/X be the inclusion functor, which we also regard as an anafunctor Jnc_{X} : Mon_{C}(X) [figure] C/X. The (LL) condition for Jnc_{X} now reads as follows: for any α ∈ C/X there is ι ∈ Mon_{C}(X) and h : α [figure] ι such that

(†) for any κ ∈ Mon_{C}(X) and any f : α  [figure] κ there is a unique f̂ : ι  [figure] κ with
f̂∘ h = f.

Actually, the last constraint is unnecessary, since it follows from k∘f = a = i∘h = k∘f̂∘h and that k is mono. Consequently, the (LL) condition for Jnc_{X} is equivalent to the existence of images in C. The left adjoint anafunctor H = Jm_{X} : C/X [figure] Mon_{C}(X) to Jnc_{X} is then, according to Lemma 2.6, given by the following. The category |H| consists of as objects, triples (α, ι, h) such that h : α [figure] ι and α ∈ C/X and ι ∈ Mon_{C}(X) which satisfies (†). In other words, A ⟶^{h} I ⟶^{i} X is an image factorisation of a : A [figure] X. A morphism (f, g) : (α, ι, h) [figure] (α′, ι′, h′) then consists of f : α [figure] α′ and g : ι [figure] ι′ such that g ∘h = h′ ∘f. Further H_{0}(α, ι, η) = α, H_{0}(f, g) = f and H_{1}(α, ι, η) = ι, H_{1}(f, g) = g.

Each anafunctor between partial orders turns out to be naturally isomorphic to an ordinary functor, and may thus be regarded simply as a monotone map. In fact, we have a slightly stronger result.

5.1. Proposition. If F : (A, ≤) [figure] (B, ≤) is some anafunctor from a preorder to a partial order, then it is naturally isomorphic to an ordinary functor G : (A, ≤) [figure] (B, ≤).

Proof. When regarding a preorder (P, ≤) as a category, we write o_{a,b} : a [figure] b for the unique arrow that exists if, and only if, a ≤ b holds. The functor G is given by G(a) = F_{1}(s) where s ∈ |F | is some object with F_{0}(s) = a. This is a good definition, since if a = F_{0}(s) = F_{0}(t), there is an isomorphism f : s [figure] t with F_{0}(f) = 1_{a}. Thus also F_{1}(f) : F_{1}(s) [figure] F_{1}(t) is an isomorphism, and hence F_{1}(s) = F_{1}(t), as B is a partial order. One shows using a similar lifting argument that G is monotone: if a ≤ a′ then there are s and s′ with a = F_{0}(s), a′ = F_{0}(s′), and hence there is some f : s [figure] s′ with F_{0}(f) = o_{a,a′} : a [figure] a′. Thereby F_{1}(f) : F_{1}(s) [figure] F_{1}(s′), that is G(s) = F_{1}(s) ≤ F_{1}(s′) = G(s′). The natural isomorphism f : F [figure] Ǧ, where Ǧ : (A, ≤) [figure] (B, ≤) is the anafunctor version of G, is given by

f_{s,t} = id_{G(t)} = o_{G(t),G(t)} : F_{1}(s) [figure] Ǧ(t)

for s ∈ |F |, t ∈ A with F_{0}(s) = (Ǧ)_{0}(t) = t.

As an application, an anafunctor Mon_{C}(X) [figure] Mon_{C}(Y) thus gives rise to an equivalent monotone map Sub_{C}(X) [figure] Sub_{C}(Y) in an obvious way using the proposition.

References

[1] S. Mac Lane. Categories for the Working Mathematician. Springer 1997.

[2] M. Makkai. Avoiding the axiom of choice in general category theory. Journal of Pure and Applied Algebra 108 (1996), 109 – 173.

[3] M. Makkai. Towards a categorical foundation of mathematics. In: Logic Colloquium ’95 (Haifa), Lecture Notes in Logic 11, Springer 1998, 153 – 190.

Department of Mathematics, Uppsala University PO Box 480, SE-751 06 Uppsala, Sweden

Email: palmgren@math.uu.se
URL: www.math.uu.se

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/20/1/20-01.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown (at) btinternet.com Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Xerox Palo Alto Research Center: paiva@parc.xerox.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca