The Limit-Colimit Coincidence for Categories

Paul Taylor

1994

Abstract

Scott noticed in 1969 that in the category of complete lattices and maps preserving directed joins, limit of a sequence of projections (maps with preinverse left adjoints) is isomorphic to the colimit of those left adjoints (called embeddings). This result holds in any category of domains and is the basis of the solution of recursive domain equations. Limits of this kind (and continuity with respect to them) also occur in domain semantics of polymorphism, where we find that we need to generalise from sequences to directed or filtered diagrams and drop the “preinverse” condition. The result is also applicable to the proof of cartesian closure for stable domains.

The purpose of this paper is to express and prove the most general form of the result, which is for filtered diagrams of adjoint pairs between categories with filtered colimits. The ideas involved in the applications are to be found elsewhere in the literature: here we are concerned solely with 2-categorical details. The result we obtain is what is expected, the only remarkable point being that it seems definitely to be about pseudo- and not lax limits and colimits.

On the way to proving the main result, we find ourselves also performing the constructions needed for domain interpretations of dependent type polymorphism.

1 Filtered diagrams

The result concerns limits and colimits of filtered diagrams of categories, so we shall be interested in functors of the form

I → FCCat^{cp}

where I is a filtered category and FCCat^{cp} is the 2-category of small categories with filtered colimits, functors with right adjoints which preserve filtered colimits and natural transformations. Since we have to perform a lot of manipulation of filtered diagrams, we begin with a short discussion on them.

Definition 1.1 A category (diagram-type) I is filtered if

(i) it is non-empty,

(ii) it has the amalgamation property for objects, i.e. given i, j ∈ I, there is some k ∈ I and u : i → k, v : j → k in I.

(iii) it has the amalgamation property for morphisms, i.e. given a parallel pair u, v : i ⇉ j in I, there is some k ∈ I and w : j → k in I with u; w = v ; w.

Example 1.2 Any category with finite colimits is filtered, for example ordinals and finite power-set lattices. The definition says that a filtered category has “weak” finite colimits.

Part of the data for the theorem is that the categories X^{i} “have filtered colimits.” We shall always take this to mean that there is a functor

colim^{↑}_{J} : X^{J} → X

which is left adjoint to the “constant functor”; the counit is the colimiting cocone and the unit (since J is connected) is an isomorphism. Often, however, we can avoid naming the colimit because we are given a cocone and set out to prove that it is colimiting, i.e. a colimit rather than the chosen colimit.

Definition 1.3 A functor F : X → Y is continuous if it preserves (commutes with) filtered colimits up to isomorphism ϕ:

colim^{↑}_{j∈J} F X_{j} \overline{ϕ_{J} ⟨X_{j}⟩ ; ≅ ; }F ( colim^{↑}_{j∈J} X_{j})

[figure: F X_{j}; σ_{j}; = = = = = = = = = = = = = =; F X_{j}; F τ_{j}]

X^{J} \overline{\begin{aligned}X & colim^{↑}_{J} \\ &  \end{aligned}}X

⇒^{ϕ}

[figure: Y^{J}; F^{J}; ^{Y} colim^{↑}_{J}; Y; F]

We shall make several uses of final subdiagrams, which generalise the idea of a cofinal subsequence of an ordinal. They is dealt with in [Mac Lane], section 9.3.

Definition 1.4 A functor U : J → I is final if for each i ∈ I the comma category i ↓ U is connected. This means that there is some j ∈ J and u : i → Uj, and if there is another j′ ∈ J with u′ : i → Uj′ then there is a “zig-zag” such that

\begin{aligned}i & = = = = = = = = = = & i & = = = = = = = = = = & i & = = = = = = = = = = & i & = = = = = = = = = = = = & i \\ Uj = & Uj_{0} & \begin{aligned}u = u_{0} \\ & \end{aligned} & \overline{Uv_{1}} & Uj_{1} & \begin{aligned}u_{1} \\ & \end{aligned} & ^{Uv_{2}} & Uj_{2} & \begin{aligned}u_{2} \\ & \end{aligned} & ⋯ & Uj_{2n−1} & \begin{matrix}u_{2n−1} \\ \end{matrix} & ^{Uv_{2n}} & Uj_{2n} & \begin{matrix}u_{2n} = u′ \\ \end{matrix} & = Uj′ \end{aligned}

commutes.

Proposition 1.5 Let D : I → X be a diagram in a category and U : J → I be a final functor. Suppose that the diagram DU : J → I → X has a colimit with cocone y_{j} : DUj → X. Then there is a unique cocone x_{i} : Di → X over the given diagram D such that x_{Uj} = y_{j}, and this is colimiting. Proof For i ∈ I, suppose j ∈ J with u : i → Uj, and put x_{i} = Du; y_{j}. We have to check that this is well-defined, by induction on the length of a zig-zag between two candidates. It suffices to consider the case of a single “zig”, u′ = u;Uv, where v : j → j′; then x_{i} = Du;y_{j} = Du;DUv;y_{j′} = Du′; y_{j′}. This also shows that x_{i} is a cocone over I. It is clearly also the only one with x_{Uj} = y_{j}.

Now let z_{i} : Di → Z be another cocone over I. Then z_{Uj} : DUj → Z is a cocone over J and, since X is the colimit, there is a unique mediator z : X → Z with y_{j} ; z = z_{Uj}. Then x_{i} ; z = Du; y_{j} ; z = Du; z_{Uj} = z_{i}, so z mediates from I also, and a fortiori it is unique. □

Definition 1.6 We shall need the following constructions on a fixed filtered category I (with typical objects):

(i) I itself

i

(ii) the coslice i_{0}/I i_{0} ^{u} i (iii) the double coslice (i_{0}, j_{0})/I

(iv) the degenerate double coslice (i_{0}, i_{0})/I

i_{0} [figure: u; v] i

(v) [a construction needed in Lemma 8.2]...

Exercise 1.7 Let I be a filtered category. Verify that the following functors are final:

(a) i_{0}/I → (i_{0}, i_{0})/I by u ↦ (u, u);

(b) (i_{0}, j_{0})/I → (v);

(c) i_{0}/I → i_{1}/I by u ↦ p; u;

(d) (i_{0}, j_{0})/I → (i_{1}, j_{1})/I by (u, v) ↦ (p; u, q ; v);

(e) I → I × I by i ↦ (i, i);

where i_{0}, i_{1}, j_{0}, j_{1} ∈ I and p : i_{1} → i_{0} and q : j_{1} → j_{0} in I. □

Exercise 1.8 Suppose I has binary coproducts. Show that the functors

(a) I → i_{0}/I by i ↦ (i_{0} → i_{0} + i), and

(a) I → (i_{0}, j_{0})/I by i ↦ (i_{0} → i_{0} + j_{0} + i ← j_{0})

(the maps being the coproduct inclusions) are final. Hence show that any colimit over i_{0}/I, (i_{0}, j_{0})/I or I × I may be calculated as a colimit over I. □

So the above assumptions about “categories with filtered colimits” may be reduced to “categories with colimits of type I”. Indeed, if we interpret the definition of filteredness constructively, any filtered category is equivalent (for the purpose of finding colimits) to a category with finite colimits.

Although we said that we wanted the categories to have all filtered colimits, it turns out that we only actually make use of colimits of diagrams of the above types. Clearly these are of essentially the same cardinality as the given diagram I, which allows us to regard filtered colimits as an algebraic operation of fixed arity. We also never consider the aggregate of all categories with filtered colimits, or perform constructions worse than products of the cardinality of I. Consequently we have no problems of size, and may treat the categories as small (or locally small); this is fortunate, considering the amount of 2-categorical work already cut out for us!

2 Pseudofunctors

In this section we shall examine the notion of pseudofunctor X^{(−)} : I^{op} → Cat. Although in the application to the limit-colimit coincidence (sections 5 and 7 onwards) we shall need I to be filtered, for the time being it may be any category whatever.

The problem is that in general for composable arrows u : i → j and v : j → k the functors

X^{u;v} and X^{u}X^{v}

cannot be expected to be equal: at best isomorphic. This is because X^{u} is typically defined by some universal property, such as pullback along u. [More generally, one may study the case where they are related by a non-invertible map one way or the other, and such constructions are called lax or oplax.] We shall find, however, that in the result which interests us we need an isomorphism

X^{u}X^{v} ^{α^{u,v}} X^{u;v}

Likewise, there is no a priori reason why X^{id} need be the identity, so we also provide an isomorphism

id_{X^{i}} ^{γ^{i}} X^{id^{i}}

(We prefer for reasons of symmetry not to put γ^{i} = id, although this is possible and quite commonly done.) Since these maps are isomorphisms, we shall feel free to define compositions involving them backwards or forwards, without writing α^{−1}.

Definition 2.1 A pseudofunctor I^{op} → Cat is an assignment of categories X^{i}, functors X^{u} : X^{j} → X^{i} and natural isomorphisms α^{u,v} and γ^{i} as above, subject to the laws

[figure: X^{u}X^{v}X^{w}; X^{u}α^{v,w}; X^{u}X^{v;w}; A; X^{u;v}X^{w}; α^{u,v}X^{w}; α^{u;v,w}; X^{u;v;w}; α^{u,v;w}]  associativity

and

[figure: X^{u}; γ^{i}X^{u}; X^{id^{i}}X^{u}; X^{u}X^{id^{j}}; X^{u}γ^{j}; X^{u}]

[figure: L; idX^{u}; R; idX^{u}]

[figure: X^{u}; α^{id_{i},u}; X^{u}; α^{u,id_{j}}]

unit

Lemma 2.2 Any well-formed diagram consisting of α’s, γ’s and their inverses commutes. Proof By induction on the length of the compositions, using the associativity and unit laws. □

Corollary 2.3 If u⃗ and v⃗ are composable strings in I with a common refinement, then there is a unique canonical isomorphism between X u⃗ =^{def} X^{u_{1}}...X^{u_{n}} and X v⃗. □

This kind of lengthy presentation of data conflicts with the spirit of category theory, and we have two alternatives: 2-functors and fibrations. (What about sheaves of categories?)

Construction 2.4 A 2-category I whose 0-cells are those of I and whose 1-cells are composable strings of arrows of I. There is a unique, invertible, 2-cell between any two strings a common refinement. We then obtain a 2-functor (no longer pseudo)

d : I^{op} → Cat by (u_{1}, ..., u_{n}) ↦ X^{u_{1}}...X^{u_{n}}

whose effect on 2-cells is well-defined by the corollary. □

Proposition 2.5 There is an isomorphism between pseudofunctors I^{op} → Cat and 2-functors I^{op} → Cat. □

Notation 2.6 Besides the equations A, L, R, etc., we shall denote the naturality square of ϕ : F → G with respect to f : X → Y by

[figure: F X; ϕX; GX; N; F Y; F f; ϕY; GY; Gf; or; F X; F f; F Y; Z; GX; ϕX; Gf; GY; ϕY]

3 Fibrations

The other approach, sometimes called the Grothendieck construction, is to form the total category Σi : I.X^{i} and display it as a fibration over I. Construction 3.1 The total category Σi : I.X^{i}.

(i) The objects of the total category are the pairs (i, X) with i ∈ I and X ∈ X^{i}; (ii) the morphisms from (i, X) to (j, Y) are the pairs (u, f) where u : i → j in I and f : X →

X^{u}Y; (iii) the identity on (i, X) is (id_{i}, γ^{i}X); (iv) the composite of (u, f) : (i, X) → (j, Y) and (v, g) : (j, Y) → (k, Z) is (u; v, f ; X^{u}g ; α^{u,v}). The display functor P : Σi : I.X^{i} → I

(v) takes (i, X) to i and (u, f) to u. The inclusion functor I_{i_{0}} : X^{i_{0}} → Σi : I.X^{i} (vi) takes X to (i_{0}, X) and f : X → Y to (id_{i_{0}}, f ; γ^{i_{0}}Y). The coherence υ_{u} : I_{i}X^{u} → I_{j} (vii) at Y ∈ X^{j} is (u, idX^{u}Y) and satisfies the equations

[figure: I_{i}; I_{i}γ^{i}; I_{i}X^{id}; U; id; I_{i}; υ_{id}; and; I_{i}X^{u}X^{v}; υ_{u}X^{v}; I_{j}X^{v}; M; I_{i}X^{u;v}; I_{i}α^{u,v}; υ_{u;v}; I_{k}; υ_{v}]

Proof First, Σi : I.X^{i} is a category. For the identities:

(u, f) ; id_{(j,Y)} = (u; id_{j}, f ; X^{u}γ^{j}Y ; α^{u,id}Y)
= (u; id_{j}, f ; id_{Y})
= (u, f)

using R and

id_{(i,X)} ; (u, f) = (id_{i} ; u, γ^{i}X ; X^{id}f ; α^{id,u}Y)
= (id_{i} ; u, f ; γ^{i}X^{u}Y ; α^{id,u}Y)
= (u, g ; id)

using naturality and L. Associativity follows from:

X^{u}(X^{v}h; α^{v,w}T) = X^{u}X^{v}h; α^{u,v}X^{w}T ; α^{u;v,w}T  A
= α^{u,v}Z ; X^{u;v}h; α^{u;v,w}T  N

Functoriality of P is obvious, as is the fact that I_{i} preserves identities; for composition:

I_{i}f ; I_{i}g = (id_{i}, f ; γ^{i}Y) ; (id_{i}, g ; γ^{i}Z)
= (id_{i}, f ; (γ^{i}Y ; X^{id}g) ; (X^{id}γ^{i}Z ; α^{id,id}Z))
= (id_{i}, f ; g ; γ^{i}Z ; id_{X^{id}Z})  Z, R

Naturality of υ:

X^{u}Y  \overline{id} X^{u}Y

[figure: X^{u}Y′; X^{u}y; X^{u}Y′; X^{u}y; X^{u}γ^{j}Y′; X^{u}X^{id}Y′]

[figure: id; L; R; α^{u,id}Y′]

[figure: X^{id}X^{u}Y′; γ^{i}X^{u}Y′; α^{id,u}Y; X^{u}Y′; id]

The U equation is essentially just L, and for M:

X^{u}X^{v}  \overline{id} X^{u}X^{v}

[figure: γ^{i}X^{u}X^{v}]  L

[figure: X^{u;v}; α^{u,v}; N; X^{id}X^{u}X^{v}; α^{id,u}X^{v}; X^{u}X^{v}; id]

A

[figure: X^{id}X^{u;v}; γ^{i}X^{u;v}; id; X^{id}X^{u;v}; X^{id}α^{u,v}; α^{id,u;v}; X^{u;v}; α^{u,v}]
□

Definition 3.2 Let P : S → I be a functor. A morphism g : Y → Z in S is

(i) vertical if P Y = P Z and P g = id_{P Y}, and

(ii) horizontal over (i.e. mapping to) v : j → k (where j = P Y, etc.) if for every h : X → Z over u; v there is a unique f : X → Y over u with h = f ; g.

The functor P is called a fibration if for every v : j → k and Z with P Z = k there is some horizontal g : Y → Z over v.

Lemma 3.3 P : Σi : I.X^{i} → I is a fibration, in which (v, g) is vertical iff v = id and horizontal iff g is invertible, the horizontal lifting of v at Z being υ_{v}Z.

Proof The only part which isn’t obvious is that if (v, g) is horizontal then g is invertible (for the converse recall that α^{u,v} is also invertible); for this we use horizontality twice with u = id_{i}. First let X_{1} = X^{v}Z, h_{1}id and derive f_{1} such that [f_{1} ; (γ^{j}Y)^{−1}] ; g = id. Then put X_{2} = Y, h_{2}g; now id and g ; [f_{1} ; (γ^{j}Y)^{−1}] both serve for f_{2}. □

Lemma 3.4 If P : S → I is a fibration then there is a factorisation system in S consisting of the (*pseudo!)vertical and horizontal maps. Proof Let h : X → Z over u : i → j. Let g : Y → Z be a horizontal lifting of u at Z and f : X → Y the unique vertical map with h = f ; g. Now if we are given v; h = k; g with v vertical and g horizontal, then h is over P h = P k ; P g and so there is a unique f over P k with f ; g = h; likewise v ; h is over P h = P k ; P g and v ; f and k both serve as the mediator, so v ; f = k. □

Exercise 3.5 Conversely, if P is any functor satisfying the definition of fibration with the word “horizontal” deleted, and the vertical and horizontal maps in S form a factorisation system, then P is a fibration.

Proposition 3.6 Σi : I.X^{i} is the lax colimit of the diagram, i.e. if N_{j} : X^{j} → Y are functors and n_{u} : N_{i}X^{u} → N_{j} natural transformations such that

id = N_{i}γ^{i} ; n_{id} and n_{u}X^{v} ; n_{v} = N_{i}α^{u,v} ; n_{u;v}

then there is a unique functor N : Σi : I.X^{i} → Y such that

NI_{i} = N_{i} and Nυ_{u} = n_{u}

Proof On objects, we are forced to put N(i, X) = N_{i}X. For morphisms we use the verticalhorizontal factorisation: (u, f) = I_{i}f ; υ_{u}Y, so we must put N(u, f) = N_{i}f ; n_{u}Y. Universality of the factorisation makes this *functorial. □

Now for the converse; clearly the category X^{i} has objects those X ∈ S with P X = i and morphisms the vertical maps over i. However, since horizontal maps are defined by a universal property, the lifting of v : j → k at Z with P Z = k is defined only up to isomorphism. We therefore have to make a choice of liftings in order to determine a functor X^{v} : X^{k} → X^{j}.

Lemma 3.7 X^{v} is *pseudofunctorial in v. □

Proposition 3.8 There is a weak equivalence from pseudofunctors I^{op} → Cat to fibrations − → I. □

4 Oplax and pseudo limits

Having established what we mean by a (pseudo)diagram of categories, we can now calculate its pseudolimit. Although we have chosen not to consider lax diagrams, we can still form a lax or oplax limit of the diagram, which corresponds to a Π-type. This has application to the construction of filtered colimits in Σ-types.

Construction 4.1 Let X^{(−)} : I^{op} → Cat be a pseudofunctor. The categories Lim i : I.X^{i} and Πi : I.X^{i} have

(i) objects the families ⟨X^{i}, x^{u}⟩ with X^{i} ∈ X^{i} for i ∈ I and x^{u} : X^{i} → X^{u}X^{j} for u : i → j such that

[figure: X^{i}; γ^{i}X^{i}; X^{id^{i}}X^{i}; U; id; X^{i}; x^{id^{i}}; and; X^{u}X^{v}X^{k}; α^{u,v}X^{k}; X^{u;v}X^{k}; M; X^{u}X^{j}; X^{u}x^{v}; x^{u}; X^{i}; x^{u;v}]

commute, where x^{u} is respectively an isomorphism and arbitrary;

(ii) morphisms from ⟨X^{i}, x^{u}⟩ to ⟨Y^{i}, y^{u}⟩ the families ⟨f^{i} : X^{i} → Y^{i}⟩ for i ∈ I such that

X^{u}X^{j} \overline{\begin{matrix}X^{u}f^{j} \\  \end{matrix}}X^{u}Y^{j}

H

[figure: X^{i}; x^{u}; f^{i}; Y^{i}; y^{u}]

commutes;

(iii) componentwise identities and composition.

(iv) There are projection functors to X^{i} given by the extraction of i-components, for which we also write X^{i}, and

(v) coherences ξ^{u} : X^{i} → X^{u}X^{j} given by extraction of u-components, which satisfy the equations

U and M

γ^{i}X^{i} = ξ^{id^{i}} and ξ^{u;v} = ξ^{u} ; X^{u}ξ^{v} ; α^{u,v}X^{k}

analogous to part (i) above. Proof Obvious. □

Lemma 4.2 Πi : I.X^{i} is isomorphic to the category of sections of the display functor Σi : I.X^{i} → I. Proof A section is a functor S : I → Σi : I.X^{i} → I such that P S = id. This means that

Si = (i, X^{i}) and Su = (u, x^{u})

where X^{i} ∈ X^{i} and x^{u} : X^{i} → X^{u}X^{j}. Functoriality corresponds exactly to the equations U and M. Likewise, a natural transformation ϕ : S → T between sections satisfies P ϕ = id, so

ϕi = (id_{i}, f^{i})

where naturality makes f^{i} : X^{i} → Y^{i} satisfy the equation H. □

Proposition 4.3 Πi : I.X^{i} is the oplax limit and Lim i : I.X^{i} is the pseudolimit. Proof Given functors F^{i} : A → X^{i} and natural transformations σ^{u} : F^{i} → X^{u}F^{j} such that the equations U and M hold:

γ^{i}F^{i} = σ^{id^{i}} and σ^{u;v} = σ^{u} ; X^{u}σ^{v} ; α^{u,v}F^{k}

then there is a unique functor F : A → Πi : I.X^{i} such that

X^{i}F = F^{i} and ξ^{u}F = σ^{u}

On objects we are forced to put F A = ⟨F^{i}A, σ^{u}A⟩, and this is an object of the oplax limit by equations U and M. Likewise on morphisms we have F a = ⟨F^{i}a⟩, with H given by N. Then F is obviously a functor and unique. Moreover σ are isomorphisms, then F factors through the inclusion Lim i : I.X^{i} ⊂ Πi : I.X^{i}. □

Proposition 4.4 The limits are Cat-enriched: if ϕ^{i} : F^{i} → G^{i} is a compatible family of natural transformations, i.e. the square

F^{i}  \overline{ϕ^{i}} G^{i}

H

[figure: X^{u}F^{j}; σ^{u}; X^{u}ϕ^{j}; X^{u}G^{j}; τ^{u}]

commutes, then there is a unique natural transformation ϕ : F → G such that ϕ^{i} = X^{i}ϕ. Proof Obvious. □

5 Continuous fibrations

In this section we assume that each X^{j} has (filtered) colimits of types I and j/I and that these are preserved by X^{u}.

Proposition 5.1 The pseudo and oplax limits have filtered colimits, which are computed componentwise and preserved by the projection functors X^{i}. Proof Let J be a filtered diagram for which each X^{i} has and X^{u} preserves colimits. For j ∈ J let ⟨X_{j}^{i}, x_{j}^{u}⟩ be an object of the oplax or pseudo limit, and for v : j → j′ let ⟨f_{v}^{i} : X_{j}^{i} → X_{j′}^{i}⟩ be a morphism, so that we have a diagram of type I in the limit. Then we also have diagrams in each X^{i}, and we may let f_{j}^{i} : X_{j}^{i} → X^{i} be a colimiting cocone.

Define x^{u} as the unique map making

[figure: X^{i}; x^{u}; X^{u}X^{i′}; X_{j}^{i}; f_{j}^{i}; x_{j}^{u}; X^{u}X_{j}^{i′}; X^{u}f_{j}^{i′}]

commute for each j ∈ J. If each x_{j}^{u} is invertible then so is x^{u}, so the result specialises from the oplax to the pseudo limit. Once we have shown that ⟨X^{i}, x^{u}⟩ is an object of the limit, this diagram immediately makes f_{j} a morphism, and it belongs to a cocone because each f_{j}^{i} does.

The *equations U and M for the object ⟨X^{i}, x^{u}⟩ are simply the colimits of the same equations for ⟨X_{j}^{i}, x_{j}^{u}⟩.

If ⟨g_{j}^{i} : X_{j}^{i} → Z^{i}⟩ is another cocone, then by the componentwise colimits we have a unique mediator g^{i} : X^{i} → Z, and this is a *morphism g = ⟨g^{i}⟩ by uniqueness of mediators X^{i} → X^{u}Z^{i′}.

□

Construction 5.2 Let ⟨X^{i}, x^{u}⟩ ∈ Πi : I.X^{i}. A diagram of type i/I in X^{i} which takes

(i →^{u} j) ^{v} (i →^{u;v} k)  to  X^{u}X^{j} ^{X^{u}x^{v}} X^{u}X^{v}X^{k} ^{α^{u,v}X^{k}} X^{u;v}X^{k}

Proof We have to check functoriality:

X^{u}X^{i} \overline{\begin{matrix}X^{u}x^{id} \\  \end{matrix}}X^{u}X^{id}X^{i}

[figure: γ^{i}; R]

[figure: X^{u}X^{i}; id U; id; X^{u}X^{i}; α^{u,id}X^{k}]

and

[figure: X^{u}X^{j}; X^{u}x^{v}; X^{u}X^{v}X^{k}; α^{u,v}X^{k}; X^{u;v}X^{k}]

M  N

[figure: X^{u}X^{v}X^{w}X^{l}; X^{u}X^{v}x^{w}; α^{u,v}X^{w}X^{l}; X^{u;v}X^{w}X^{l}; X^{u;v}x^{w}]

[figure: X^{u}α^{v,w}X^{l}]  A

[figure: X^{u}X^{v;w}X^{l}; X^{u}x^{v;w}; α^{u,v;w}X^{l}; X^{u;v;w}X^{l}; α^{u;v,w}X^{l}]
□

Definition 5.3 Let Y^{i} be the colimit with cocone z^{u} : X^{u}X^{j} → Y^{i}, i.e.

X^{u}X^{j}  \overline{z^{u}} Y^{i}

E

[figure: X^{u}X^{v}X^{k}; X^{u}x^{v}; α^{u,v}X^{k}; X^{u;v}X^{k}; z^{u;v}]

commutes for all u ∈ i/I.

Construction 5.4 An isomorphism y^{t} : Y^{i′} ≅ X^{t}Y^{i}. Proof Let t : i′ → i in I. There is a diagram of type i/I given by applying X^{t} to the previous construction, and since this functor is continuous, X^{t}z^{u} is a colimiting cocone. Using ZA, α^{t,u}X^{j} ; z^{t;u} : X^{t}X^{u}X^{j} → Y^{i′} is a cocone, so there is a unique mediator X^{t}Y^{i} → Y^{i′}. Now (α^{t,u}X^{j})^{−1} ; X^{t}z^{u} : X^{t;u}X^{j} → Y^{i} is a cocone over a final subdiagram of the diagram defining Y^{i′} and so extends to a cocone over the whole diagram, whose mediator y^{t} : Y^{i′} → X^{t}Y^{i} is the inverse. This is the unique map such that

[figure: Y^{i′}; y^{t}; X^{t}Y^{i}; F; X^{t;u}X^{j}; z^{t;u}; α^{t,u}X^{j}; X^{t}X^{u}X^{j}; X^{t}z^{u}]  over j/I

commutes for all u : i → j, the vertical maps forming colimiting cocones.

Lemma 5.5 ⟨Y^{i}, y^{u}⟩ is an object of Lim i : I.X^{i} ⊂ Πi : I.X^{i}. Proof For the U equation:

Y^{i}  \overline{\begin{matrix}y^{id} =? \\ γ^{i}Y^{i} \end{matrix}} X^{id}Y^{i}

N

[figure: X^{u}X^{j}; z^{u}; \underline{α^{id,u}X^{j}}; γ^{i}X^{u}X^{j}; X^{id}X^{u}X^{j}; X^{id}z^{u}]

which is the colimit of U, and the associative law is obtained in the same way:

X^{u}X^{v}Y^{k}  \overline{α^{u,v}Y^{k}} X^{u;v}Y^{k}
[figure: X^{u}X^{v}z^{w}; N; X^{u;v}z^{w}]
X^{u}X^{v}X^{w}X^{l} \overline{\begin{matrix}α^{u,v}X^{w}X^{l} \\  \end{matrix}}X^{u;v}X^{w}X^{l}
F  A  F
[figure: X^{u}X^{v;w}X^{l}; X^{u}α^{u,v}X^{l}; α^{u,v;w}X^{l}; X^{u;v;w}X^{l}; α^{u;v,w}X^{l}]
[figure: X^{u}z^{v;w}; F; z^{u;v;w}]
[figure: X^{u}Y^{j}; X^{u}y^{v}; y^{u}; Y^{i}; y^{u;v}]
□

Construction 5.6 Morphism ζ : ⟨X^{i}, x^{u}⟩ → ⟨Y^{i}, y^{u}⟩ by ζ^{i} = γ^{i}X^{i} ; z^{id^{i}}. Proof It is a morphism:

X^{i}  \overline{x^{u}} X^{u}X^{j} = = = = = = = = = X^{u}X^{j} = = = = = = = = = X^{u}X^{j}
Z  L  R
[figure: X^{id}X^{i}; γ^{i}X^{i}; X^{id}x^{u}; X^{id}X^{u}X^{j}; γ^{i}X^{u}X^{j}; α^{id,u}X^{j}; X^{u}X^{j}; id; α^{u,id}X^{j}; X^{u}X^{id}X^{j}; X^{u}γ^{i}X^{j}]

E

[figure: Y^{i}; z^{id^{i}}; = = = = = = = = = = = = = = = = = = = = = = = = = = =; Y^{i}; z^{u}; y^{u}; X^{u}Y^{j}; X^{u}z^{id^{j}}]
□

Lemma 5.7 ζ is universal into the pseudolimit. Proof Suppose ⟨b^{i}⟩ : ⟨X^{i}, x^{u}⟩ → ⟨A^{i}, a^{u}⟩ is a morphism with a^{u} invertible, so the square

X^{i}  \overline{b^{i}} A^{i}

H

[figure: X^{u}X^{j}; x^{u}; X^{u}b^{j}; X^{u}A^{j}; a^{u}]

commutes. I claim that X^{u}b^{j} ; (a^{u})^{−1} is a cocone for the diagram defining Y^{i}:

[figure: X^{u}X^{j}; X^{u}b^{j}; X^{u}A^{j}; a^{u}; A^{i}]

H

[figure: X^{u}X^{v}X^{k}; X^{u}x^{u}; X^{u}X^{v}b^{k}; X^{u}X^{v}A^{k}; X^{u}a^{v}; M]

Z

[figure: X^{u;v}X^{k}; α^{u,v}X^{k}; X^{u;v}b^{k}; X^{u;v}A^{k}; α^{u,v}A^{k}; a^{u;v}; A^{i}; ‖]

Hence there is a unique mediator c^{i} : Y^{i} → A^{i} such that

Y^{i}  \overline{c^{i}} A^{i}

G

[figure: X^{u}X^{j}; z^{u}; X^{u}b^{j}; X^{u}A^{j}; a^{u}]

commutes. Finally the following diagram shows that c : Y → A is a morphism:

Y^{i}  \overline{c^{i}} A^{i}

[figure: z^{u}]  G

[figure: F; X^{u}X^{j}; X^{u}b^{j}; X^{u}A^{j}; a^{u}]

X^{u}X^{i}dX^{j}^{α^{u,id}X^{j} }U \begin{matrix}X^{u}γ^{j}X^{j} \\  \end{matrix}\overline{X^{u}X^{id}b^{j}} X^{u}X^{id}A^{j} \begin{aligned}Z & X^{u}γ^{j}A^{j} \\ &  \end{aligned}

[figure: X^{u}z^{id}]  G

[figure: X^{u}Y^{j}; y^{u}; X^{u}c^{j}; X^{u}A^{j}; X^{u}a^{id} X^{u}γ^{j}A^{j}]
□

Proposition 5.8 The full inclusion functor Lim i : I.X^{i} ⊂ Πi : I.X^{i} is continuous and has a reflection (left adjoint post-inverse). Proof The first part is immediate from Proposition 5.1; note also that the inclusion is full because the two categories have the same definition of morphisms. We have just found the unit of the adjunction; observe that if x⃗ are already isomorphisms then ζ is also an isomorphism. □

There is an application of these results to finding filtered colimits in Σ-types.

Definition 5.9 A functor P : S → C is a continuous fibration if (i) it is a fibration,

(ii) the fibres X^{i} have, and the functors X^{u} preserve, filtered colimits (of types J),

(iii) C has filtered colimits (of types I), and

(iv) if c_{i} : C_{i} → C is a colimiting cocone for a diagram c_{u} of type I then X^{c_{i}} is a pseudolimiting cone.

Lemma 5.10 An object over a colimit is the colimit of its liftings. Proof Let c_{i} : C_{i} → C be a colimiting cocone in C and X ∈ X^{C}. Let υ_{c_{i}}X : ⟨C_{i}, X^{i}⟩ → ⟨C, X⟩ be the horizontal lifting of c_{i}, where X^{i} = X^{c_{i}}X; then with x^{u} = υ_{c_{u}} we have an object of Πi : I.X^{C_{i}}. By (iv) this corresponds to an object Y ∈ X^{C} with X^{i} ≅ X^{c_{i}}Y... □

Proposition 5.11 If P : S → C is a continuous fibration then S has and P preserves filtered colimits (of type I). Proof We are given I → S, a diagram of type I, and suppose that the fibration P corresponds to a pseudofunctor C^{op} → Cat. Write

C^{(−)} : I → S → C and X^{(−)} : I^{op} → S^{op} → C^{op} → Cat

so that the diagram has vertices X_{i} ∈ X^{i}. The arrows of the diagram are of the form x^{u} : X^{i} → X^{u}X^{j} and satisfy the *equations, and so we have an object of Πi : I.X^{i}. Applying the reflector yields an object ⟨Y^{i}, y^{u}⟩ of Lim i : I.X^{i}, which corresponds to a unique object Y (up to isomorphism) of the fibre over C = colim^{↑} C_{i}. By the lemma, Y is the colimit of Y⃗, and from the reflection it is also the colimit of the X⃗. (explain why) □

Every object is the colimit of its liftings; the colimiting cocone of a diagram of horizontal maps is horizontal.

6 Adjunctions

Recall that we call two functors h : A → B, c : B → A adjoint, and write c ⊣ h, if there is a bijection

\frac{cB → A}{B → hA}

which is natural in A and B. In particular, corresponding to id : cB → cB there is the unit ηB : B → hcB and to id : hA → hA the counit ϵA : chA → A. These are natural in A and satisfy the triangular identities:

[figure: c; cη; chc; hch; ηh; h]

[figure: X; id; Y; id]

[figure: c; ϵc; h; cϵ]

[Mac Lane 1971], §4.1 shows that (c, h, η, ϵ) suffice to characterise the adjunction. Since we no longer have any mention of the objects of the categories A and B, the latter may now be objects of an abstract 2-category C, and we have an equational definition of an adjunction between two opposite arrows (1-cells) between two objects (0-cells) of a 2-category.

The above natural bijection is a well-known and easy to remember way of presenting the adjunction, but it has a less well known dual. Instead of applying c and h to objects of (or functors into) A and B, we can apply functors out of these categories:

\frac{B̂h → Â}{B̂ → Âc}

naturally in Â : A → X and B̂ : B → X. We could say “h is co-left adjoint to c.”

Construction 6.1 A natural bijection between natural transformations θ : h_{1} → h_{2} and ϕ : c_{2} → c_{1} which identifies identities. Using both correspondences together we obtain

[figure: h_{2}c_{2}h_{1}; η_{2}h_{1}; h_{1}; ιh_{1}; h_{2}c_{1}h_{1}]

[figure: c_{2}h_{2}; h_{2}κ; h_{2}ϵ_{1}; h_{1}c_{1}]

[figure: ϵ_{2}; h_{2}; θ; θc_{1}]

[figure: c_{2}h_{1}; c_{2}θ; κ; id; h_{2}c_{1}; ι; id; η_{1}]

[figure: ϵ_{1}; c_{1}; h_{2}ϕ]

[figure: c_{1}h_{1}; ϕh_{1}; κc_{1}; ϵ_{2}c_{1}; h_{2}c_{2}; η_{2}]

[figure: c_{2}h_{1}c_{1}; c_{2}η_{1}; c_{2}; ϕ; c_{2}ι; c_{2}h_{2}c_{1}]

(commutation of one of which suffices) where we can verify θ ↦ ι ↦ ϕ ↦ κ ↦ θ are bijections using the triangle laws. □

We shall write

id  \overline{η_{1}} h_{1}c_{1}

D

[figure: h_{2}c_{2}; η_{2}; h_{2}ϕ; h_{2}c_{1}; θc_{1}]

Lemma 6.2 The bijection respects composition and identites. Proof It suffices to show that θ; θ′ and ϕ′ ; ϕ satisfy the equation.

id  \overline{η_{1}} h_{1}c_{1}

[figure: η_{2}] D

[figure: D′; h_{2}c_{2}; h_{2}ϕ; h_{2}c_{1}; θc_{1}]

Z

[figure: h_{3}c_{3}; η_{3}; h_{3}ϕ′; h_{3}c_{2}; θ′c_{2}; h_{3}ϕ; h_{3}c_{1}; θ′c_{1}]

The result for identities is obvious. □

Definition 6.3 The 2-category C^{⊣} has the same objects as C; its 1-cells are adjunctions (c, h, η, ϵ) and its 2-cells are pairs of natural transformations (ϕ, θ) satisfying the equations of the construction. The composition is in the obvious way.

Proposition 6.4 The forgetful 2-functor C^{⊣} → C which extracts the left (or right) part of the adjunction and natural transformations is full and faithful at the 2-level. Loosely speaking, the 2-categories of left and right adjoints are dual. □

Note carefully that we shall find it convenient to write composition in I both right-handedly as u; v and left-handedly v ∘ u: these notations are completely synonymous. We shall also adopt the convention of writing X^{u} for the functors in the limit diagram (which are contravariant in u) and X_{u} for their left adjoints in the colimit diagram (which are covariant in u).

Definition 6.5 Let P : S → C be a functor. A morphism f : X → Y is op-horizontal over P f = u : i → j if for any h : X → Z over u; v : i → j → k there is a unique g : Y → Z over v with h = f ; g. We call P an op-fibration if each u has an op-horizontal lifting at each X with P X = i. If P is both a fibration and an op-fibration we call it a bifibration.

Lemma 6.6 P : S → C is an op-fibration iff P : S^{op} → C^{op} is a fibration. Proof Obvious. □

Proposition 6.7 Let X^{(−)} : I^{op} → Cat be a pseudofunctor. Then P : Σi : I.X^{i} is a bifibration iff each X^{u} has a left adjoint, written X_{u}.

Note 6.8 Since the left adjoints (op-substitutions) X_{u} are covariant in u : i → j, but we still write composition of functors from right to left, it is convenient to use the notations

u; v and v ∘ u

synonymously for the composite i →^{u} j →^{v} k. Proof

[⇒] Any morphism (u, f) : (i, X) → (j, Y) can be factorised as a vertical followed by a horizontal, or as an op-horizontal followed by a vertical:

(i, X) \overline{}(j, X_{u}X)

[figure: (u, f)]

[figure: (i, X^{u}Y); (j, Y)]

where X_{u}X is introduced as the codomain of the op-horizontal lifting. Making such a choice for all X ∈ X^{i}, we can extend this uniquely to a functor X_{u} : X^{i} → X^{j}. I claim this is the left adjoint: f corresponds bijectively to either vertical part X → X^{u}Y or X_{u}X → Y. The unit and counit are given by

X

[figure: ophoriz]

[figure: X^{u}X_{u}X; η^{u}X; horiz; X_{u}X]

and

X_{u}X^{u}Y

[figure: ophoriz]

[figure: X^{u}Y; horiz; Y; ϵ_{u}Y]

and the equations η^{u}X^{u} ; X^{u}ϵ_{u} = id and X_{u}η^{u} ; ϵ_{u}X_{u} = id may be verified using the universal properties of the horizontal map X^{u}Y → Y and the op-horizontal map X → X_{u}X respectively.

[⇐] I claim that (u, η^{u}X) : (i, X) → (j, X_{u}X) is op-horizontal. Let (u ; v, f) : (i, X) → (k, Z), so that f′ = f ; (α^{u,v}Z)^{−1} : X → X^{u}X^{v}Z in X^{i}. Let f′′ : X_{u}X → X^{v}Z be its adjoint transpose; this is the unique solution of f′ = η^{u}X ; X^{u}f′′. Then (v, f′′) : (j, X_{u}X) → (k, Z) is the required factorisation. □

Lemma 6.9 The functors X_{u} have coherences δ_{i} : X_{id} → id and β_{v,u} : X_{v∘u} → X_{v}X_{u} which satisfy equations dual to those in definition 2.1:

[figure: X_{w}X_{v}X_{u}; X_{w}β_{v,u}; X_{w}X_{v∘u}; A; X_{w∘v}X_{u}; β_{w,v}X_{u}; β_{w∘v,u}; X_{w∘v∘u}; β_{w,v∘u}]  associativity

and

[figure: X_{u}; δ_{j}X_{u}; X_{id_{j}}X_{u}; X_{u}X_{id_{i}}; X_{u}δ_{i}; X_{u}]

[figure: L; idX_{u}; R; idX_{u}]

[figure: X_{u}; β_{id_{j},u}; X_{u}; β_{u,id_{i}}]

unit

Proof Immediate from lemmas 3.7 and 6.8. □

Lemma 6.10 The coherences α^{u,v}, β_{v,u}, γ^{i} and δ_{i} are related to the units by the *equations

id  \overline{\begin{matrix}η^{id} \\  \end{matrix}}X^{id}X_{id}

C

[figure: id; id; γ^{k}; X^{id}; X^{id}δ_{k}]

and

[figure: id; η^{w}; X^{w}X_{w}; X^{w}η^{w′}X_{w}; X^{w}X^{w′}X_{w′}X_{w}; B; X^{w;w′}X_{w′∘w}; η^{w;w′}; X^{w;w′}β_{w′,w}; X^{w;w′}X_{w′}X_{w}; α^{w,w′}X_{w′}X_{w}]

and to the counits by the equations

id ^{ϵ_{id}} X_{id}X^{id}

C

[figure: id; id; δ_{k}; X_{id}; X_{id}γ^{k}]

and

[figure: id; ϵ_{w′}; X_{w′}X^{w′}; X_{w′}ϵ_{w}X^{w′}; X_{w′}X_{w}X^{w}X^{w′}; B; X_{w′∘w}X^{w;w′}; ϵ_{w′∘w}; β_{w′,w}X^{w;w′}; X_{w′}X_{w}X^{w;w′}; X_{w}X_{w′}α^{w,w′}]

□

7 Transfer functors

Now we shall begin the construction of the equivalence between the pseudolimit and pseudocolimit. Imagining for the moment that we already have this equivalence, we can form

X^{i} ^{X_{i}} Colim_{k∈I} X^{k} ∼ Lim_{k∈I} X^{k} ^{X^{j}} X^{j}

using the colimiting cocone and limiting cone. It is our purpose now to construct this composite functor, M_{i}^{j}. When we have it we can use the universal property of the pseudolimit to construct functors X^{i} → Lim k : I.X^{k}; these will be left adjoints to X^{i} and will form the colimiting cocone X_{i}.

Construction 7.1 A Diagram of type (i, j)/I of functors X^{i} → X^{j}. On objects, (i →^{u} k ←^{v} j) ↦ X^{v}X_{u}. The image of w : k → k′ is

[figure: X^{v}X_{u}; X^{v}η^{w}X_{u}; X^{v}X^{w}X_{w}X_{u}; α^{v,w}X_{w}X_{u}; X^{v;w}X_{w}X_{u}]

N

[figure: X^{v}X^{w}X_{w∘u}; X^{v}X^{w}β_{w,u}; α^{v,w}X_{w∘u}; X^{v;w}X_{w∘u}; X^{v;w}β_{w,u}; = X^{v′}X_{u′}]

Proof We have to show that we have defined a functor. The effect on the identity id_{k} is the long anticlockwise route from X^{v}X_{u} on the top left to X^{v}X_{u} on the top right. We use the correspondence between γ^{k} and δ_{k}, together with one unit and one counit law.

[figure: X^{v}X_{u}; id; X^{v}X_{u}; id; X^{v}X_{u}]

C  [figure: R; α^{v,id}]

[figure: X^{v}X^{id}X_{id}X_{u}; η^{id}; δ_{k}; X^{v}X^{id}X_{u}; γ^{k}]

[figure: R; id]

X^{v}X^{id}X_{u}^{β_{id,u} }

For the composite w; w′,

X^{v}X_{u} = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = X^{v}X_{u}

B

[figure: X^{v}X^{w}X_{w}X_{u}; η^{w}; η^{w′}; X^{v}X^{w}X^{w′}X_{w′}X_{w}X_{u}; α^{w,w′}; X^{v}X^{w;w′}X_{w′}X_{w}X_{u}; β_{w′,w}; X^{v}X^{w;w′}X_{w′∘w}X_{u}; η^{w;w′}]

Z  A  Z

[figure: X^{v;w}X_{w}X_{u}; α^{v,w}; η^{w′}; X^{v;w}X^{w′}X_{w′}X_{w}X_{u}; α^{v,w}; α^{v;w,w′}; X^{v;w;w′}X_{w′}X_{w}X_{u}; α^{v,w;w′}; β_{w′,w}; X^{v;w;w′}X_{w′∘w}X_{u}; α^{v,w;w′}]

N  N  A

[figure: X^{v;w}X_{w∘u}; β_{w,u}; η^{w′}; X^{v;w}X^{w′}X_{w′}X_{w∘u}; β_{w,u}; α^{v;w,w′}; X^{v;w;w′}X_{w′}X_{w∘u}; β_{w,u}; β_{w′,w∘u}; X^{v;w;w′}X_{w′∘v∘u}; β_{w′∘w,u}]

where the left-hand side is the effect on w, the bottom that on w′ and the right-hand side that on w; w′. □

Construction 7.2 Functor M_{i}^{j} : X^{i} → X^{j} is the (pointwise) colimit, with cocone ν_{u}^{v} : X^{v}X_{u} → M_{i}^{j}, i.e.

X^{v}X_{u}  \overline{ν_{u}^{v}} M_{i}^{j}

K

[figure: X^{v}X^{w}X_{w}X_{u}; X^{v}η^{w}X_{u}; α^{v,w}X_{w}X_{u}; X^{v;w}X_{w}X_{u}; X^{v;w}β_{w,u}; X^{v;w}X_{w∘u}; ν_{w∘u}^{v;w}]

Proof We know that (i, j)/I is a filtered category, so it is possible to form the colimit M_{j}^{i}X for each X; it is standard that this extends to a functor which is the colimit in the functor category. In detail, for f : X → Y we have a cocone X^{v}X_{u}f ; ν_{u}^{v}Y : X^{v}X_{u}X → M_{j}^{i}Y by naturality of η^{w}, α^{v,w} and β_{w,u}, so M_{j}^{i}f is the unique mediator and it is automatic that ν_{u}^{v} is natural. □

Construction 7.3 Coherences μ_{s}^{t} : X^{t}M_{i}^{j}X_{s} ≅ M_{i′}^{j′} for s : i′ → i and t : j′ → j such that

X^{t}M_{i}^{j}X_{s}  \overline{μ_{s}^{t}} M_{i′}^{j′}

P

[figure: X^{t}X^{v}X_{u}X_{s}; X^{t}ν_{u}^{v}X_{s}; α^{t,v}X_{u}X_{s}; X^{t,v}X_{u}X_{s}; X^{t;v}β_{u,s}; X^{t;v}X_{u∘s}; ν_{u;s}^{t;v}]

Proof The lower composite X^{t}X^{v}X_{u}X_{s} → M_{i′}^{j′} is a cocone by naturality of α, β and η and associativity of α and β (the proof is very similar to the diagram in 7.1). Since X^{t} is continuous, X^{t}ν_{u}^{v}X_{s} is colimiting and μ_{s}^{t} is then defined as the mediator. It is invertible because (i, j)/I → (i′, j′)/I is final, and natural by the universal property of the colimit. □

Lemma 7.4 The coherences μ_{i}^{t} = X^{t}M_{i}^{j}δ_{i} ; μ_{id_{i}}^{t} : X^{t}M_{i}^{j} ≅ M_{i′}^{j′} for s : i′ → i satisfy U, M and

X^{t}M_{i}^{j}  \overline{μ_{i}^{t}} M_{i′}^{j′}

P

[figure: X^{t}X^{v}X_{u}; X^{t}ν_{u}^{v}X_{s}; α^{t,v}X_{u}; X^{t,v}X_{u}; ν_{u;s}^{t;v}]

Proof These are just colim^{↑} UX_{u} and colim^{↑} MX_{u}. □

Definition 7.5 X_{i} : X^{i} → Lim k : I.X^{k} such that X^{j}X_{i} = M_{i}^{j} and ξ^{u}X_{i} = μ_{i}^{u}. We use the coherences μ_{i}^{t} and the universal property of the pseudolimit. □

8 Unit and counit

Now we shall show that X_{i} ⊣ X^{i} and that X_{i} is a colimiting cocone.

Lemma 8.1 The maps

X^{v}X_{u}X^{i} X^{v}X_{u}ξ^{u} ; ≅ X^{v}X_{u}X^{u}X^{k} ^{X^{v}ϵ_{u}X^{k}} X^{v}X^{k} ξ^{v} ; ≅ X^{j}

form a cocone for the diagram defining M_{i}^{j}X^{i}.

Proof Recall that X_{d,e,f}^{a,b,c} =^{def} X^{a}X^{b}X^{c}X_{d}X_{e}X_{f}, and we also omit the functors applied to natural transformations. Then the diagram

[figure: X_{u}^{v}X^{i}; ξ^{u}; X_{u}^{v}X^{u,k}; ϵ_{u}; X^{v,k}; ξ^{v}; X^{j}]

[figure: Z; Z; η^{w}; ξ^{w}]

[figure: X_{w,u}^{v,w}X^{i}; η^{w}; ξ^{u}; X_{w,u}^{v,w}X^{u,k}; η^{w}; ϵ_{u}; X_{w}^{v,w}X^{k}; N; X^{v,w,l}]

[figure: ξ^{u;w}; M; ξ^{w}; N; ξ^{w}; η^{w}]

[figure: X_{w,u}^{v,w}X^{u;w,l}; α^{u,w}; X_{w,u}^{v,w}X^{u,w,l}; ϵ_{u}; X_{w}^{v,w}X^{w,l}; Y; M]

[figure: Z; β_{w,u}; B; ϵ_{w}]

[figure: X_{w∘u}^{v,w}X^{i}; β_{w,u}; ξ^{u;w}; X_{w∘u}^{v,w}X^{u;w,l}; ϵ_{w∘u}; X^{v,w,l}; id]

Z  Z

[figure: X_{w∘u}^{v;w}X^{i}; α^{v,w}; ξ^{u;w}; X_{w∘u}^{v;w}X^{u;w,l}; α^{v,w}; ϵ_{w∘u}; X^{v;w,l}; α^{v,w}; ξ^{v;w}; X^{j}; ‖]

commutes. □

Definition 8.2 Natural transformation ϵ_{i}^{j} : M_{i}^{j}X^{i} → X^{j} is the mediator, the unique map such that

M_{i}^{j}X^{i}  \overline{ϵ_{i}^{j}} X^{j}

Q

[figure: X^{v}X_{u}X^{i}; ν_{u}^{v}X^{i}; X^{v}X_{u}ξ^{u}; X^{v}X_{u}X^{u}X^{k}; X^{v}ϵ_{u}X^{k}; X^{v}X^{k}; ξ^{v}]

commutes.

Construction 8.3 ϵ_{i} : X_{i}X^{i} → id_{Lim} such that ϵ_{i}^{j} = X^{j}ϵ_{i}. Proof The coherence equation H is obtained by varying the above diagram along t : j′ → j, which is the colimit of three commutative squares which amount to naturality of α^{t,v} and M for ξ. □

Lemma 8.4 The diagram

M_{i}^{j}M_{i}^{i}  \overline{ϵ_{i}^{j}} M_{i}^{j}
Q  [figure: μ_{i}^{v}]
[figure: X_{u}^{v}M_{i}^{i}; ν_{u}^{v}; μ_{i}^{u}; X_{u}^{v}X^{u}M_{i}^{k}; ϵ_{u}; X^{v}M_{i}^{k}]
P N P
[figure: X_{u}^{v}X_{u}^{u,id}; ν_{k}^{id}; ϵ_{u}; X_{u}^{v,id}; ν_{u}^{id}]
[figure: α^{u,id}; R; N; α^{v,id}; R]
[figure: X_{u}^{v}X_{u}^{u}; ν_{u}^{u}; id; X_{u}^{v}X_{u}^{u}; γ^{k}; ϵ_{u}; X_{u}^{v}; γ^{k}; id; X_{u}^{v}; ν_{u}^{v}]

commutes. □ Lemma 8.5 ϵ_{i} : X_{i}X^{i} → 1_{L} is a colimiting cocone. Proof *Cocone (over what?) Colimiting: use finality.

[colim^{↑}_{i∈I} X_{i}X^{i}]^{j}  \overline{}X_{j} = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = X_{j}

[figure: X^{j}X_{i}X^{i}; = = = = = =; X^{j}X_{i}X^{i}; ϵ_{i}^{j}; X^{v}X^{k}; ξ^{j}]

[figure: X^{v}X_{u}X^{i}; ν_{u}^{v}X^{i}; = u = id_{k}; X^{v}X_{id}X^{k}; X^{v}X_{id}ξ^{id}; X^{v}X^{id}X_{id}X^{k}; X^{v}ϵ_{id}X^{k}]

The details are in the diagram defining ϵ_{i}^{j}. *Cocones, *coherences. □ Lemma 8.6 η^{u} ; ν_{u}^{u} : id_{X^{i}} → M_{i}^{i} = X^{i}X_{i} is independent of the choice of u : i → j. Proof It suffices to show that η^{u} ; ν_{u}^{u} = η^{id_{i}} ; ν\begin{matrix}id & i \\ id & i \end{matrix}. This follows from definition 7.2 (of ν) with w = id, together with the U and C equations for γ^{i} and δ_{i}. □ Definition 8.7 η^{i} = η^{u} ; ν_{u}^{u}. Lemma 8.8 η^{i}X^{i} ; X^{i}ϵ_{i} = id_{X^{i}}.

Proof

M_{i}^{i}X^{i}  \overline{ϵ_{i}^{i} = X^{i}ϵ_{i}} X^{i}

Q

[figure: X^{id^{i}}X_{id_{i}}X^{i}; ν\begin{matrix}id & i \\ id & i \end{matrix}X^{i}; X^{id^{i}}X_{id_{i}}ξ^{id^{i}}; X^{id^{i}}X_{id_{i}}X^{id^{i}}X^{i}; X^{v}ϵ_{id_{i}}X^{i}; X^{v}X^{k}; ξ^{id^{i}}]

Z  [figure: Y; id]

[figure: X^{i}; η^{id_{i}}X^{i}; ξ^{id}; X^{u}X^{i}; η^{id_{i}}X^{id^{i}}X^{i}]
□

Lemma 8.9 X_{i}η^{i} = ϵ_{i}X_{i}. Proof By enrichment of the pseudo limit, it suffices to verify componentwise that M_{i}^{j}η^{i}; ϵ_{i}^{j}X_{i} = id_{M_{i}^{j}}. The diagram

[figure: M_{i}^{j}; M_{i}^{j}η^{i}; M_{i}^{j}M_{i}^{i}; ϵ_{i}^{j}X_{i}; M_{i}^{j}]

Z

X_{u}^{v}M_{i}^{i}^{ν_{u}^{v}M_{i}^{i} }

[figure: η]

[figure: X_{u}^{v}; ν_{u}^{v}; η; X_{u}^{v}X_{u}^{u}; X_{u}^{v}ν_{u}^{u}; X^{v}ϵ_{u}X_{u}; X_{u}^{v}; ν_{u}^{v}]

commutes for all (u, v) ∈ (i, j)/I; the bottom row is the identity by X. The left-hand side is part of a colimiting cocone, and the diagram and provides another cocone for which the top row and the identity both serve as the mediator. □

Lemma 8.10 Lim i : I.X^{i} is the pseudo-colimit, with cocone X_{i}. Proof Let G_{i} : X^{i} → A be another cocone for this diagram with coherences ... Consider the diagram of type I of functors Lim i : I.X^{i} → A with i ↦ A_{i}X^{i} which takes u : i → j to

Functoriality... Let A be the colimit. Then

AX_{i} = colim^{↑}_{j} A_{j}M_{i}^{j} = colim^{↑}_{j} colim^{↑}_{(u,v)∈I/(i,j)} A_{j}X^{v}X_{u} ≅ colim^{↑}_{u:k→i} A_{k}X_{u} = A_{i}

*Uniqueness. □

9 Pseudolimit of adjunctions

Finally we shall show that we have the limit in the category of homomorphisms. Let G^{i} : X → X^{i} be a cone of homomorphisms and F_{i} ⊣ G^{i} be the corresponding comparisons, with units υ^{i} and counits δ_{i}. Since L is the limit we have a unique mediating functor G : X → L with G^{i} = GX^{i}, and similarly, since it is also the colimit, F : L → X with F_{i} = F X_{i}.

Construction 9.1 Natural transformations υ : id_{L} → GF and δ : F G → id_{X}, by the diagrams

[figure: id_{L}; υ; GF; X_{k}X^{k}; ϵ_{k}; X_{k}υ^{k}X^{k}; X_{k}G^{k}F_{k}X^{k}; ϵ_{k}GF ϵ_{k}; sF G; δ; id_{X}; δ_{k}; F_{k}G^{k}; F ϵ_{k}G]

Lemma 9.2 F ⊣ G with unit υ and counit δ. Proof The two triangle laws follow from these diagrams:

[figure: F; F υ; F GF; δF; F; F_{k}X^{k}; X_{k}υ^{k}X^{k}; F_{k}G^{k}F_{k}X^{k}; δ_{k}F_{k}X^{k}; F_{k}X^{k}]

and

[figure: G^{j}; X^{j}υG; G^{j}F G; G^{j}δ; G^{j}]

[figure: M_{i}^{j}G^{i}; M_{i}^{j}G^{i}F_{i}G^{i}; M_{i}^{j}G^{i}]

[figure: X^{v}X_{u}G^{j}; X^{v}X_{u}υ^{i}G^{i}; X^{v}X_{u}G^{i}F_{i}G^{i}; X^{v}X_{u}G^{i}δ_{i}; X^{v}X_{u}G^{i}]
□

Theorem 9.3 For any cofiltered diagram of homomorphisms, the limit of the homomorphisms quâ continuous functors, the colimit of the comparisons quâ continuous functors and the limit of the homomorphisms quâ homomorphisms exist and are naturally equivalent. Proof It only remains to formulate and prove naturality. One way of stating this is that the forgetful functors FCCat^{hm} → FCCat and FCCat^{hm} → FCCat^{op} create limits. □

We call L the bilimit of the diagram.

10 Notes

Definition 8.2:

X^{k}  \overline{ξ^{v}} X^{v}X^{l}
Q  [figure: X^{v}ϵ_{w′}X^{l}]
[figure: M_{j}^{k}X^{j}; ϵ_{i}^{k}; ν_{w;u}^{v}X^{j}; X^{v}X_{w∘u}X^{j}; X^{v}X_{w∘u}ξ^{u}; X^{v}X_{w′}X^{w′}X^{l}]
N  M
[figure: M_{j}^{k}X^{u}X^{i}; M_{j}^{k}ξ^{u}; ν_{w;u}^{v}X^{u}X^{i}; X^{v}X_{w∘u}X^{u}X^{i}; X^{v}X_{w∘u}ξ^{u}; ξ; X^{v}X_{w∘u}X^{u}X^{w}X^{l}; α]
[figure: μ_{u}^{k}X^{u}X^{i}]  P
[figure: X^{id}M_{i}^{k}X_{u}X^{u}X_{i}; X^{id}ν_{u}^{v}; X^{id}X_{w}^{v}X^{v}X_{u}X^{u}X_{i}; α; X^{v}X_{w}X_{u}X^{u}X^{i}; β; N]
[figure: γ^{k}; Z; γ]
[figure: M_{i}^{k}X_{u}X^{u}X^{i}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ν_{u}^{v}X_{u}X^{u}X_{i}; X^{v}X_{w}X_{u}X^{u}X^{i}; id; X_{wu}^{v}X^{uw}ξ^{w}; X^{v}X_{w}X_{u}X^{u}X^{w}X^{l}; β]
N  Z
[figure: M_{i}^{k}X^{i}; M_{i}^{k}ϵ_{u}X^{i}; ν_{u}^{v}X^{i}; X^{v}X_{w}X^{i}; X^{v}ϵ_{w}ϵ_{u}X^{i}; X^{v}X_{w}ξ^{w}; X^{v}X_{w}X^{l}; X^{v}X_{w}ϵ_{u}X^{w}X^{l}]
Q  [figure: X^{v}ϵ_{w}X^{l}]
[figure: X^{k}; ϵ_{i}^{k}; ξ^{v}; X^{v}X^{l}; B]

Construction 9.1:

[figure: id; δ; F G; F_{k}G^{k} = F_{k}X^{k}G; δ_{k}; F X_{k}X^{k}G; F ϵ_{k}G; X^{i}; A_{i}; σ_{u} ⇓ A; A_{j}; X^{j}; X_{u}]

[figure: Lim X^{i}; A; X^{i}; A_{i}; X^{i}; = ξ^{u} ⇒  = σ_{u} ⇒; X^{j}; X^{u}; X_{u}; A_{i}; A_{i}X^{i}; τ_{i}; A_{j}X_{u}X^{u}X^{j}; σ_{u} · ξ^{u}; A; τ_{j}; A_{j}X^{j}; A_{j}ϵ_{u}X^{j}]

[figure: AX_{i}; σ_{i}; A_{i}X^{i}X_{i}; τ_{i}X_{i}; A_{i}η^{i}; A_{i}ϵ_{i}; A_{i}; A_{i}η^{u}; A_{i}X^{u}X_{u}; A_{i}ν_{u}^{u}; A_{i}; A_{j}X_{u}; σ_{u}; A_{j}X_{u}η^{u}; A_{j}X_{u}X^{u}X_{u}; σ_{u}X^{u}X_{u}; A_{j}ϵ_{u}X^{u}; A_{j}X_{u}; σ_{u}; AX_{i}; σ_{i} ; ≅; A_{i}; A_{i}τ_{i}; A_{i}ϵ^{i}; A_{i}X_{i}X^{i}]

[figure: AX_{j}X_{u}; Aι_{u}; AX_{i}; A_{j}X_{u}; σ_{j}X_{u}; σ_{u}; A_{i}; σ_{i}; A; τ_{i}; Aϵ_{i}; A_{i}X^{i}; σ_{i}X^{i}; AX_{i}X^{i}]

A

[figure: Aϵ_{i}]

[figure: A_{i}X^{i}; τ_{i}; σ_{i}X^{i}; AX_{i}X^{i}]

N

[figure: A_{i}X_{u}X^{u}X^{i}; A_{i}ϵ_{i}X^{i}; σ_{i}X_{u}X^{u}X^{i}; AX_{i}X_{u}X^{u}X^{i}; AX_{i}ϵ_{i}X^{i}]

pseudo − colim

[figure: A_{j}X^{j}; σ_{u}ξ^{u}; σ_{j}X^{j}; AX_{j}X^{j}; Aι_{u}ξ^{u}]

υ^{i}F^{i} ; F^{i}δ_{i} = idF^{i} υ^{i} : id_{X^{i}} → F^{i}G_{i} δ_{i} : G_{i}F_{i} → id_{A} θ_{i} : G_{i} → GX_{i}

[figure: F^{i}; υ^{i}F^{i}; F^{i}G_{i}F^{i}; F^{i}δ_{i}; F^{i}]

def  def

[figure: adj; X^{i}X_{i}F^{i}; η^{i}F^{i}; X^{i}υX_{i}X^{i}F; X^{i}F GX_{i}X^{i}F; X^{i}F θ_{i}X^{i}F; X^{i}F Gϵ_{i}F; X^{i}F GF; X^{j}F δ]

N  [figure: id]

[figure: id; X^{i}F; ϵ_{i}F^{i}; X^{i}υF; X^{i}F GF; X^{i}F Gϵ_{i}F]

\begin{aligned}A \\ & [figure: G_{i}] ⊣ [figure: F^{i}] \\ & X^{i} \\ & [figure: X_{i}] ⊣ [figure: X^{i}] \\ Lim & \begin{aligned}G & \\ & ⊣ \begin{matrix}F \\ \end{matrix} \end{aligned} \end{aligned}

[figure: id_{X^{i}}; υ^{i}; X^{i}F G_{i}; def; X^{i}X_{i}; η^{i}; X^{i}νX_{i}; X^{i}F GX_{i}; X^{i}F θ_{i}; X^{v}X_{u}; ν_{u}^{v}]

G_{i}F^{i}  \overline{δ_{i}} id_{A}

def

GX_{i}F^{i} = GX_{i}X^{i}F

\begin{aligned}θ_{i}F^{i} = & θ_{i}X^{i}F \\ & \end{aligned}

Gϵ_{i}F colimiting
GF

δ . . . . . . . . . . . . . . . .

[figure: G_{i}; G_{i}υ^{i}; G_{i}F^{i}G_{i}; δ_{i}G_{i}; G_{i}]

Z  def

[figure: GX_{i}; θ_{i}; GX_{i}υ^{i}; GX_{i}X^{i}F G_{i}; θ_{i}F^{i}G_{i}; Gϵ_{i}F G_{i}; GF G_{i}; δG_{i}]

def  N  N

[figure: GX_{i}X^{i}X_{i}; GX_{i}η^{i}; GX_{i}X^{i}υX_{i}; GX_{i}X^{i}F GX_{i}; GX_{i}X^{i}F_{i}θ_{i}; Gϵ_{i}F GX_{i}; GF GX_{i}; GF θ_{i}]

Z

[figure: GX_{i}; Gϵ_{i}X_{i}; GυX_{i}; GF GX_{i}; Gϵ_{i}F GX_{i}; δGX_{i}; GX_{i}; δGX_{i}; θ_{i}]