BRICS RS-01-27 Cáccamo & Winskel: A Higher-Order Calculus for Categories BRICS

Basic Research in Computer Science

A Higher-Order Calculus for Categories

Mario Jose Cáccamo Glynn Winskel BRICS Report Series RS-01-27 ISSN 0909-0878 June 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Mario Jose Cáccamo & Glynn Winskel.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/01/27/

A Higher-Order Calculus for Categories

Mario Cáccamo  Glynn Winskel

June, 2001

Abstract

A calculus for a fragment of category theory is presented. The types in the language denote categories and the expressions functors. The judgements of the calculus systematise categorical arguments such as: an expression is functorial in its free variables; two expressions are naturally isomorphic in their free variables. There are special binders for limits and more general ends. The rules for limits and ends support an algebraic manipulation of universal constructions as opposed to a more traditional diagrammatic approach. Duality within the calculus and applications in proving continuity are discussed with examples. The calculus gives a basis for mechanising a theory of categories in a generic theorem prover like Isabelle.

1 Introduction

A language for category theory [11] together with a calculus to derive natural isomorphisms are presented. We systematise categorical judgements of the kind: an expression is functorial in its free variables; there is an isomorphism between two expressions natural in their free variables. The resulting logic gives the foundations for a mechanisation of category theory in a generic theorem prover like Isabelle [15].

The language is based on the simply typed λ-calculus [2] where types denote categories and expressions functors between categories. We introduce constants, for hom-sets, for example, and binders for ends and coends. Ends are a generalisation of limits and play a central role in the calculus in increasing its expressive power.

The rules of the calculus enable a mechanical manipulation of formulae with ends and their dual coends. This gives a more calculational approach to categories than is usual, and less dependence on diagrams. This approach supplies tools for proving preservation of limits and colimits.

One motivation behind this work is the increasing use of the machinery of category theory in denotational semantics. There categories are often seen as generalised domains. An application of special interest to us is the use of presheaf categories as models for concurrency. A central result there is that functions between presheaf categories which preserve colimits, a form of continuity, preserve open-map bisimulation [9] (see [7] for details).

2 The Language

2.1 Categories as Types

In general, a category C consists of a class of objects and a class of arrows between any pair of objects A, B, written C(A, B), which support composition and have identities. If the class of arrows between any pair of objects is a set we say that C is locally small and call C(A, B) the hom-set for A, B. We will concentrate on locally small categories.

Locally small categories together with functors, arrows between categories, themselves form the large category CAT. Furthermore, given two locally small categories C and D, the functors from C to D also form a category in which the objects are the functors and the arrows between them are natural transformations. We can summarise the rich structure of CAT in the diagram

[figure: C; F; G; θ; D]

where F and G are functors between locally small categories C and D, and θ is a natural transformation from F to G.^{1} We shall be particularly concerned with those natural transformations between functors which are isomorphisms, so-called natural isomorphisms.

The structure of CAT suggests a language. Its types will denote locally small categories; so we expect judgements which express the legitimate ways to build up types. Its expressions with free variables will denote functors from the category where the variables range to the category where the expression belongs; there will be judgements saying that expressions are functorial in their free variables. The diagram above suggests terms and judgements for constructing natural transformations. Here we will however restrict attention to just the judgements of there being a natural isomorphism between functors denoted by expressions. We plan to extend this work to a notation for natural transformations. Despite just considering natural isomorphisms, the calculus is surprisingly useful, allowing us to derive, for example, results on preservation of limits.

1In fact, making CAT an example of a 2-category.

The constructors for types are interpreted as operations over categories. Given the categories C and D,

• the opposite C^{op} is the category whose objects are the objects of C and whose arrows are the arrows in C reversed, i.e., C^{op}(A, B) = C(B, A) for any pair of objects A, B;

• the product C × D is the category whose objects and arrows are ordered pairs of objects and arrows in C and D;

• the sum C + D is the category whose objects and arrows are given by the disjoint union of objects and arrows in C and D; and

• the functor category [C, D] is the category of functors from C to D and the natural transformation between them.

Observe that a functor category built out of locally small categories is not necessarily locally small (Crole discusses this point in [8, page 61]). We constrain the use of functor categories [C, D] to the case where C is small. A locally small category is small when the collection of objects is a set. Simple examples of small categories are 0 and 1, the empty and singleton categories respectively. We write ℂ, 𝔻, 𝕀, 𝕁, ⋯ for small categories.

The syntax for types as locally small categories is

C ::= Set | 0 | 1 | C^{op} | C_{1} × C_{2} | C_{1} + C_{2} | [ℂ, C] .

Thus, for the language locally small category and type are synonymous.

2.2 Syntax for Expressions

The expressions E_{1}, E_{2}, ⋯ are defined by

E ::=X | 1 | λX^{ℂ}.E | E_{1}(E_{2}) | C(E_{1}, E_{2}) | (E_{1}, E_{2}) |
fst(E) | snd(E) | inl(E) | inr(E) | case^{C+D}(E_{1}, E_{2}, E_{3}) |
E_{1} × E_{2} | E_{1} + E_{2} | ∫_{X^{ℂ^{op}},Y^{ℂ}} E | ∫^{X^{ℂ^{op}},Y^{ℂ}} E

where C, D and ℂ are types, and X is drawn from a countably infinite set of variables. The constant 1 stands for the singleton set.

The syntax is that of the simply typed λ-calculus à la Church with products and sums. To simplify the notation we sometimes ommit the type annotations in the lambda abstractions. The “integral” binders denote ends and coends. Ends extend the concept of limit to functors of mixed variance with domain of the form ℂ^{op} × ℂ. The treatment of ends given in this work supports a mechanical manipulation of these binders whose properties resemble the properties of the integral in mathematical analysis. Ends are discussed later – they are a central notion of the language for categories.

2.3 Functoriality

Not all possible expressions in the language give rise to functors. An example of a non-functorial expression is C(X, X) for a nontrivial category C; there is no action over arrows matching the action over objects. Welltyped expressions in the language represent those expressions functorial in their free variables.

The syntactic judgement X_{1} : C_{1}, ⋯, X_{n} : C_{n} ⊢ E : C says that the expression E of type C is functorial in the free variables occurring in the context X_{1} : C_{1}, ⋯, X_{n}: C_{n}; i.e. it denotes a functor from C_{1} × … × C_{n} to C. A context is a finite sequence of variable declarations. In informal mathematical usage one says E(X_{1}, ⋯, X_{n}) is functorial in X_{1}, ⋯, X_{n}. Thus, an expression-in-context has two possible readings: as an object when the free variables are interpreted as objects, and as an arrow when the free variables are interpreted as arrows.

From the typing rules we derive well-typed expressions enforcing functoriality. One example is the rule for hom-expressions:

hom \frac{Γ ⊢ E_{1} :C Γ′ ⊢ E_{2} :C}{Γ^{op}, Γ′ ⊢ C(E_{1}, E_{2}):Set}

where Γ and Γ′ are contexts^{2} and Γ^{op} is obtained from Γ by replacing each occurrence of a type C by C^{op}. We insist, also in the syntax, that (C^{op})^{op} = C and that forming the opposite category respects the type constructions so e.g. (C × D)^{op} = C^{op} × D^{op} and [C, D]^{op} = [C^{op}, D^{op}].

The rule for lambda abstraction introduces functor categories:

lam \frac{Γ, X:ℂ ⊢ E:D}{Γ ⊢ λX^{ℂ}.E:[ℂ, D]}

with the assumption that ℂ is small. If E is an expression with free variables W, Z, we abbreviate λX^{ℂ×𝔻}.E[fst(X)/W, snd(X)/Z] as λW^{ℂ}, Z^{𝔻}.E.

There is a symmetric rule for eliminating functor categories:

app \frac{Γ ⊢ F:[ℂ, D] Γ′ ⊢ E:ℂ}{Γ, Γ′ ⊢ F (E):D.}

The derivation below shows X: ℂ ⊢ λY^{ℂ^{op}}.ℂ(Y, X) : [ℂ^{op}, Set] which denotes the so-called Yoneda functor for ℂ:

Y :ℂ ⊢ Y :ℂ ass X:ℂ ⊢ X:ℂ ass
X:ℂ, Y :ℂ^{op} ⊢ ℂ(Y, X):Set

hom + exc

X:ℂ ⊢ λY^{ℂ^{op}}.ℂ(Y, X):[ℂ^{op}, Set]

lam

where the rule (exc) allows us to permute the variables in the contexts (there are rules for weakening and contraction as well).

2.4 Naturality

Given two expressions E_{1}(X_{1}, ⋯, X_{n}) and E_{2}(X_{1}, ⋯, X_{n}) functorial in the variables X_{1}, ⋯, X_{n} it is sensible to ask whether the associated functors are naturally isomorphic. When they are, one says

E_{1}(X_{1}, ⋯, X_{n}) ≅ E_{2}(X_{1}, ⋯, X_{n})

natural in X_{1}, ⋯, X_{n}. More formally, the syntactic judgement Γ ⊢ E_{1} ≅ E_{2} : C says the expressions E_{1} and E_{2}, where Γ ⊢ E_{1} : C and Γ ⊢ E_{2} : C, are naturally isomorphic in the variables of Γ. The judgement Γ ⊢ E_{1} ≅ E_{2} :C asserts the existence of a natural isomorphism between the functors denoted by E_{1} and E_{2}.

2The variables that appear in a context are distinct and different contexts have disjoint set of variables; any conflict is avoided by renaming.

The relation defined by isomorphism is an equivalence, and there are rules for reflexivity, symmetry and transitivity. The rules for isomorphisms encode useful facts in category theory. There are, for example, rules for the Yoneda lemma and its corollary:

Theorem 2.1 (Yoneda lemma) Let C be a locally small category. Then

[C^{op}, Set](λX.C(X, C), F ) ≅ F (C)

natural in C ∈ C and F ∈ [C^{op}, Set].

A special case of the Yoneda lemma is expressed by the rule

yon \frac{Γ, X:ℂ^{op} ⊢ E:Set}{Γ, Z:ℂ^{op} ⊢ E[Z/X] ≅ [ℂ^{op}, Set](λX^{ℂ^{op}}.ℂ(X, Z), λX^{ℂ^{op}}.E):Set .}

That the Yoneda functor is full and faithful follows by replacing F in Theorem 2.1 with the functor λX.C(X, D) for some D in C. This, together with the fact that full and faithful functors preserve isomorphisms, gives:

Corollary 2.2 C ≅ D iff λX.C(X, C) ≅ λX.C(X, D) for C, D ∈ C.

This is encoded in the calculus by the rule:

rep \frac{Γ, X:C^{op} ⊢ C(X, E_{1}) ≅ C(X, E_{2}):Set}{Γ ⊢ E_{1} ≅ E_{2} :C}

with the assumption that X is not free in E_{1} or E_{2}. A complete presentation of the rules is postponed until section 4.

3 Ends and Coends

3.1 Representability

The manipulation of ends relies on the theory of representable functors.

Definition 3.1 (Representable Functor) A functor F : C^{op} → Set is representable if for some object C in C there is an isomorphism

C(X, C) ≅ F (X)

natural in X.

A representation for F : C^{op} → Set is a pair (C, θ) such that

C(X, C) ≅^{θ_{X}} F (X)

natural in X. A trivial example of a representable functor is λX.C(X, A) for some object A in C. There is a dual definition for G : C → Set: a representation for G is a pair (D, ψ) such that

C(D, X) ≅^{ψ_{X}} G(D)

natural in X. Below we see that limits and more generally ends are representations for special functors. The next result is a consequence of the Yoneda functor being full and faithful (see [6] for a proof):

Theorem 3.2 (Parametrised Representability) Let F : A × B^{op} → Set be a functor such that for every object A in A there exists a representation (B(A), θ^{A}) for the functor λX.F (A, X), then there is a unique extension of the mapping A ↦ B(A) to a functor λX.B(X) : A → B such that

B(X, B(A)) ≅^{(θ^{A})_{X}} F (A, X)

is natural in A ∈ A and X ∈ B^{op}.

This result shows that representations are functorial in their parameters; this will be crucial in justifying the typing rules for end formulae.

3.2 Limits and Ends as Representations

Definition 3.3 (Limit) A limit of a functor F : 𝕀 → C is a representation (L, θ) for λX.[𝕀, C](λY.X, F) : C^{op} → Set, i.e.,

C(X, L) ≅^{θ_{X}} [𝕀, C](λY.X, F)  (1)

natural in X ∈ C^{op}.

The object L in (1) is often written in the literature as \underleftarrow{lim}_{𝕀} F and called the limit of F. The right hand side of (1) is the set of natural transformations from the constant functor λY.X to F. Given γ ∈ [𝕀, C](λY.X, F) and an arrow u : I → J in 𝕀 the naturality condition ensures that the diagram

\xymatrix{ & F (I) \ar[dd]^{F (u)} \\ X \ar[ur]^{γ_{I}} \ar[dr]^{γ_{J}} \\  & F (J)}

commutes. A natural transformation of this kind is a cone from X to F. The isomorphism θ_{X} in (1) establishes a one-to-one correspondence between arrows from X to L and cones from X to F. From the naturality condition on X we recover the more concrete definition of limits where θ_{L}(id_{L}) is the universal cone. Dually, a colimit for F : 𝕀 → C is a representation for the functor λX.[𝕀, C](F, λY.X) : C → Set.

The notion of end extends that of limit to functors of mixed-variance, e.g. with domain 𝕀^{op} × 𝕀. In this setting, cones are generalised to wedges. Given a functor G : 𝕀^{op} × 𝕀 → D, a wedge β from X to G is a family of arrows ⟨β_{I} : X → G(I, I)⟩_{I∈𝕀} in D such that for any arrow u : I → J in 𝕀 the diagram

\xymatrix{ & G(I, I) \ar[dr]^{G(id_{I},u)} \\ X \ar[ur]^{β_{I}} \ar[dr]_{β_{J}} &  & G(I, J) \\  & G(J, J) \ar@{-->}[ur]_{G(u,id_{J})}}

commutes. Just as cones are natural transformations, so are wedges dinatural transformations – see [11, page 218] for the definition of dinatural transformations. Dinatural transformations do not compose in general, but they do compose with natural transformations. So there is a functor

λF, G.Dinat(F, G) : [𝕀^{op} × 𝕀, D]^{op} × [𝕀^{op} × 𝕀, D] → Set

where Dinat(F, G) is the set of dinatural transformations from F to G. A wedge from X to G is an element in Dinat(λY.X, G).

Definition 3.4 (End) An end of a functor G : 𝕀^{op} × 𝕀 → D is a representation (E, θ) for λX.Dinat(λY.X, G) : D^{op} → Set, i.e.,

D(X, E) ≅^{θ_{X}} Dinat(λY.X, G)  (2)

natural in X ∈ D^{op}.

Following a similar analysis to that with limits, we may recover a more concrete definition for ends where θ_{E}(id_{E}) is the universal wedge. In the language for categories the object E in (2) is written as ∫_{X^{𝕀^{op}},Y^{𝕀}} G(X, Y), and more informally, and economically, as ∫_{Z^{𝕀}} G(Z^{−}, Z^{+}) where Z^{−} : 𝕀^{op} and Z^{+} : 𝕀.

Dually, a coend of G : 𝕀^{op} × 𝕀 → C is a representation for the functor λX.Dinat(G, λY.X). We write ∫^{X^{𝕀^{op}},Y^{𝕀}} G(X, Y) for the coend of G (more informally, ∫^{Z^{𝕀}} G(Z^{−}, Z^{+})).

3.3 Ends with Parameters

A special case of parametrised representability arises when considering ends as representations. Suppose the functor F : A×𝕀^{op}×𝕀 → B such that for any object A in A the induced functor λX, Y.F (A, X, Y) : 𝕀^{op}×𝕀 → B has as end the representation (∫_{Z^{𝕀}} F (A, Z^{−}, Z^{+}), θ^{A}). Then the mapping A ↦ ∫_{Z^{𝕀}} F (A, Z^{−}, Z^{+}) extends uniquely to a functor from A to B such that

B(X, ∫_{Z^{𝕀}} F (A, Z^{−}, Z^{+})) ≅^{(θ^{A})_{X}} [𝕀^{op} × 𝕀, B]((λY, W.X), (λY, W.F (A, Y, W)))

natural in A ∈ A and X ∈ B^{op}. This is just Theorem 3.2 applied to the functor λA, X.[𝕀^{op} × 𝕀, B]((λY, W.X), (λY, W.F (A, Y, W))). We conclude that the process of taking ends does not disturb functoriality over the variables which remain free. This justifies the rule for ends:

int \frac{Γ, X:ℂ^{op}, Y :ℂ ⊢ E:D}{Γ ⊢ ∫_{X^{ℂ^{op}},Y^{ℂ}} E:D}

where D is complete, i.e., D has all ends (and equivalently, all limits).

Limits correspond to ends where the functor is extended with a dummy argument.^{3} Thus, by using the rules (int), weakening (wea) and exchange (exc) we can form the derivation:

{Γ, Y :ℂ ⊢ E:D \atop Γ, X:ℂ^{op}, Y :ℂ ⊢ E:D} wea + exc
Γ ⊢ ∫_{X^{ℂ^{op}},Y^{ℂ}} E:D .

int As the variable X is not free in the expression E the last judgement might be abbreviated as just Γ ⊢ ∫_{Y^{ℂ}} E: D. Hence, we can use the integral for both ends and limits.

3Conversely, an end can be regarded as a limit: given a functor F : 𝕀^{op} × 𝕀 → C there is a category 𝕀^{§} together with a functor d^{§} : 𝕀^{§} → 𝕀^{op}×𝕀 such that ∫_{I^{𝕀}} F (I^{−}, I^{+}) ≅ \underleftarrow{lim}_{𝕀}(F ∘ d^{§}); for the details of this construction see [6, 11].

3.4 Complete Categories

We restrict the application of rules for ends to complete categories. A category is complete when it has all limits. The category Set, for example, is complete.

The set of natural transformations from F to G is characterised by an end expression, the so-called naturality formula:

[𝕀, D](F, G) ≅ ∫_{I^{𝕀}} D(F (I^{−}), G(I^{+}))

natural in F ∈ [𝕀, D]^{op} and G ∈ [𝕀, D]. This isomorphism is explained by giving a concrete choice for the end in Set (see [6, 11] for details). In the calculus there is a rule for this formula:

nat \frac{Γ, X:ℂ ⊢ E_{1} :D Γ′, Y :ℂ ⊢ E_{2} :D}{Γ^{op}, Γ′ ⊢ [ℂ, D](λX^{ℂ}.E_{1}, λY^{ℂ}.E_{2}) ≅ ∫_{X^{ℂ^{op}},Y^{ℂ}} D(E_{1}, E_{2}):Set .}

Similarly, there is an end expression for dinatural transformations:

Dinat(F, G) ≅ ∫_{I^{𝕀}} D(F (I^{+}, I^{−}), G(I^{−}, I^{+}))  (3)

natural in F ∈ [𝕀^{op} × 𝕀, D]^{op} and G ∈ [𝕀^{op} × 𝕀, D]. By composing the isomorphism for the definition of ends (2) with an instance of the dinaturality formula (3) where F is a constant functor, we obtain the isomorphism:

D(X, ∫_{I^{𝕀}} G(I^{−}, I^{+})) ≅ ∫_{I^{𝕀}} D(X, G(I^{−}, I^{+}))  (4)

natural in X ∈ D^{op} and G ∈ [𝕀^{op} × 𝕀, D]. This formula shows how ends can be moved outside of a hom-expression. To avoid the introduction of special syntax for dinaturals in the language for categories we adopt (4) as the definition for ends:

end \frac{Γ, X:ℂ^{op}, Y :ℂ ⊢ E:D}{Γ, W:D^{op} ⊢ D(W, ∫_{X^{ℂ^{op}},Y^{ℂ}} E) ≅ ∫_{X^{ℂ^{op}},Y^{ℂ}} D(W, E):Set}

where D is complete.

The definition of limits is derivable from (end), (nat) and weakening (wea). First we derive a special case of the naturality formula:

\begin{matrix}W:D ⊢ W:D & ass \\ W:D, X:ℂ ⊢ W:D \end{matrix}wea ⋮ . ; Γ, Y :ℂ ⊢ E:D

Γ, W:D^{op} ⊢ [ℂ, D](λX^{ℂ}.W, λY^{ℂ}.E) ≅ ∫_{X^{ℂ^{op}},Y^{ℂ}} D(W, E):Set .

nat + exc

This is combined by means of transitivity of isomorphism with

Γ, W:D^{op} ⊢ D(W, ∫_{X^{ℂ^{op}},Y^{ℂ}} E) ≅ ∫_{X^{ℂ^{op}},Y^{ℂ}} D(W, E):Set .

Finally (with some rewriting):

Γ, W:D^{op} ⊢ D(W, ∫_{Y^{ℂ}} E) ≅ [ℂ, D](λX^{ℂ}.W, λX^{ℂ}.E):Set .

An important result in reasoning about ends is the Fubini theorem:

fub \frac{Γ, X:𝕀^{op}, Y :𝕀, W:𝕁^{op}, Z:𝕁 ⊢ E:D}{Γ ⊢ ∫_{X^{𝕀^{op}},Y^{𝕀}} ∫_{W^{𝕁^{op}},Z^{𝕁}} E ≅ ∫_{W^{𝕁^{op}},Z^{𝕁}} ∫_{X^{𝕀^{op}},Y^{𝕀}} E:D}

where D is complete.

3.5 Duality: Coend Formulae

In CAT, any functor F : C → D is mirrored by its dual, a functor F^{∗} : C^{op} → D^{op} which acts, as a function, in exactly the same way as F on objects and arrows. This dual view also involves natural transformations and is given by applying the 2-functor (−)^{∗} : CAT → CAT, which acts

[figure: C; F; G; θ; D; C^{op}; F^{∗}; G^{∗}; θ^{∗}; D^{op} ,]

where the components of θ^{∗} are opposites of the components of θ. Note that dualising twice gives the identity. (Although (−)^{∗} reverses natural transformations, this does not have a direct effect in the calculus since we are only concerned with natural isomorphisms.)

Like a mirror, dualising affects our view of things and the way we describe them. A judgement Γ ⊢ E : D denotes a functor whose dual is described by a dual form of judgement, Γ^{op} ⊢ E^{∗} : D^{op}, where E^{∗} is the expression obtained by turning ends into coends and coends into ends in E, adjusting the types of the bound variables. For example, the dual form of Z : C ⊢ ∫_{X^{𝕀^{op}},Y^{𝕀}} E : D is Z : C^{op} ⊢ ∫^{Y^{𝕀^{op}},X^{𝕀}} E^{∗} : D^{op} where E is an expression with free variables amongst X, Y, Z. The dual form of a product E_{1} × E_{2} in Set is the sum E_{1}^{∗} + E_{2}^{∗} in Set^{op}. It follows that (E^{∗})^{∗} = E. In a similar way we can dualise judgements about the existence of natural isomorphisms, and so embody dualisation in the rules:

dua\frac{Γ ⊢ E:D}{Γ^{op} ⊢ E^{∗}:D^{op}} duaI\frac{Γ ⊢ E_{1} ≅ E_{2} :D}{Γ^{op} ⊢ E_{1}^{∗} ≅ E_{2}^{∗}:D^{op}.}

We can now, for example, derive the rule (int*) for typing coends:

Γ, X:ℂ^{op}, Y :ℂ ⊢ E:D
Γ^{op}, Y :ℂ^{op}, X:ℂ ⊢ E^{∗}:D^{op}

dua + exc

Γ^{op} ⊢ ∫_{Y^{ℂ^{op}},X^{ℂ}} E^{∗}:D^{op}

int

Γ ⊢ ∫^{X^{ℂ^{op}},Y^{ℂ}} E:D.

dua

A judgement for Γ^{op}, Γ′ ⊢ C(E_{1}, E_{2}) : Set where Γ ⊢ E_{1} : C and Γ′ ⊢ E_{2} : C denotes the composition of the functor C(−, +) : C^{op} × C → Set with the functors E_{1}^{∗} : Γ^{op} → C^{op} and E_{2} : Γ → C. Notice that, in keeping with practice, an expression occurring on the left of a hom-expression is implicitly dualised. This affects the definition of substitution of expressions for free variables.

The substitution E_{1}[E_{2}/X] replaces the negative occurrences of the free variable X (on the left in an odd number of hom-expressions) by E_{2}^{∗} and other occurrences by E_{2}. Formally, a substitution E_{1}[E_{2}/X] is defined by induction on the structure of E_{1} where the defining clause for hom-expressions is

C(E′, E′′)[E_{2}/X] = C(E′[E_{2}^{∗}/X], E′′[E_{2}/X]).

Because C(X, Y) ≅ C^{op}(Y, X), for X : C^{op}, Y : C, by substitution and dualisation we obtain the rule

opp\frac{Γ ⊢ E_{1} :C Γ′ ⊢ E_{2} :C}{Γ^{op}, Γ′ ⊢ C(E_{1}, E_{2}) ≅ C^{op}(E_{2}^{∗}, E_{1}^{∗}):Set.}

Thus, there is a derivation

\overline{_{0 small}}  \overline{_{1 small}}  \frac{C small}{C^{op} small}

\frac{C small D small}{C × D small}  \frac{C small D small}{C + D small}

\overline{_{Set complete}}  \frac{D complete}{[C, D] complete}

Figure 1: Some rules for smallness and completeness.

Γ, X:ℂ^{op}, Y :ℂ ⊢ E:D
Γ^{op}, Y :ℂ^{op}, X:ℂ ⊢ E^{∗}:D^{op}

dua + exc

Γ^{op}, W:D ⊢ D^{op}(W, ∫_{Y^{ℂ^{op}},X^{ℂ}} E^{∗}) ≅ ∫_{Y^{ℂ^{op}},X^{ℂ}} D^{op}(W, E^{∗}):Set.

end

Using (opp) twice and transitivity we obtain the derived rule

end*\frac{Γ, X:ℂ^{op}, Y :ℂ ⊢ E:D}{Γ^{op}, W:D ⊢ D(∫^{X^{ℂ^{op}},Y^{ℂ}} E, W) ≅ ∫_{Y^{ℂ^{op}},X^{ℂ}} D(E, W):Set.}

We have chosen to formalise dualisation in rules and then derive rules for coends. By starting out with sufficient extra rules for coends we could eliminate the dualisation rules from any derivation.

4 The Calculus

4.1 Rules for Typing

To avoid the set-theoretic paradoxes, categories are classified according to their size as small and locally small. The formalisation of this distinction demands a form of judgement for types: C is small where C is any type. Similarly, the rules involving end expressions make assumptions about completeness asking for judgements: C is complete and C is cocomplete where C is any type.

With a view to keeping the presentation of the rules compact, assumptions about types have been presented rather informally. In Fig. 1, however, the basic set of formal rules is shown. Rules for other constants than Set should be added. This point is not elaborated here; a natural extension to this work is to design a richer language for types.

In Fig. 2 we show the typing rules for expressions. These rules are interpreted as operations on functors, taking the functors denoted by the premises to that denoted by the conclusion. Such an interpretation yields a categorical semantics in the usual sense (see [1, 5, 8]).

The rule for assumption (ass) is interpreted as the identity functor which exists for any category. The interpretation of the rule for weakening (wea) takes the functor Γ ⟶^{E} C denoted by the premise of the rule to the composition Γ×Γ′ ⟶^{π_{Γ}} Γ ⟶^{E} C which denotes the conclusion. We can interpret the rules for exchange and contraction similarly.

The rule for pairs (pai) corresponds to the application of the product functor − × − : CAT × CAT → CAT to the interpretation of E_{1} and E_{2}. The projections (fst) and (snd) are just the composition with the projection arrows associated to the product. The rules for introduction and elimination of sums are interpreted through the functor − + − : CAT × CAT → CAT in a similar fashion. The rule (dua) expresses the application of the functor (−)^{∗} to Γ ⟶^{E} C.

The abstraction rule (lam) is interpreted by “currying” the functor denoted by E, i.e., a variable from the context is shifted into the expression. Symmetrically the evaluation functor justifies the rule (app). The rule for substitution (sub) corresponds to the composition of functors; recall substitution may involve dualisation – see § 3.5.

The rules (ten) and (uni) have a special status. Products in Set are introduced with a view to a more general model given by V-enriched categories, where V is a monoidal closed category equipped with a tensor product ⊗. In the case of Set, the tensor product is the categorical product.

4.2 Rules for Natural Isomorphisms

The rules for natural isomorphisms are listed in Fig. 3. The structural rules for weakening, exchange and contraction are defined as usual and not shown. The rules describe how to build natural isomorphisms. For example, the premise of the rule (lamI)

X_{1} :C_{1}, ⋯, X_{n}:C_{n}, X:C ⊢ E_{1} ≅ E_{2} :D

ass \overline{X:C ⊢ X:C}  dua \frac{Γ ⊢ E:D}{Γ^{op} ⊢ E^{∗}:D^{op}}
wea \frac{Γ ⊢ E:C}{Γ, Γ′ ⊢ E:C}  exc \frac{Γ ⊢ E:C}{Π(Γ) ⊢ E:C} Π permutation

con \frac{Γ, X:C, Y :C ⊢ E:D}{Γ, Z:C ⊢ E[Z/X, Z/Y]:D} Z is fresh

fst \frac{Γ ⊢ E:C × D}{Γ ⊢ fst(E):C}  snd \frac{Γ ⊢ E:C × D}{Γ ⊢ snd(E):D}

pai \frac{Γ ⊢ E_{1} :C Γ′ ⊢ E_{2} :D}{Γ, Γ′ ⊢ (E_{1}, E_{2}):C × D}

inl \frac{Γ ⊢ E:C}{Γ ⊢ inl(E):C + D}  inr \frac{Γ ⊢ E:D}{Γ ⊢ inr(E):C + D}

cas \frac{Γ ⊢ E_{1} :C + D Γ′ ⊢ E_{2} :E Γ′′ ⊢ E_{3} :E}{Γ, Γ′, Γ′′ ⊢ case_{C+D}(E_{1}, E_{2}, E_{3}):E}

lam \frac{Γ, X:C ⊢ E:D C small}{Γ ⊢ λX^{C}.E:[C, D]} app \frac{Γ ⊢ F:[C, D] Γ′ ⊢ E:C C small}{Γ, Γ′ ⊢ F (E):D}
hom \frac{Γ ⊢ E_{1} :C Γ′ ⊢ E_{2} :C}{Γ^{op}, Γ′ ⊢ C(E_{1}, E_{2}):Set}  sub \frac{Γ, X:C ⊢ E_{1} :D Γ′ ⊢ E_{2} :C}{Γ, Γ′ ⊢ E_{1}[E_{2}/X]:D}
uni \overline{⊢ 1:Set}  ten \frac{Γ ⊢ E_{1} :Set Γ′ ⊢ E_{2} :Set}{Γ, Γ′ ⊢ E_{1} × E_{2} :Set}

int \frac{Γ, X:C^{op}, Y :C ⊢ E:D D complete C small}{Γ ⊢ ∫_{X^{C^{op}} ,Y^{C}} E:D}

Figure 2: Typing rules.

ref \frac{Γ ⊢ E:C}{Γ ⊢ E ≅ E:C}  sym \frac{Γ ⊢ E_{1} ≅ E_{2} :C}{Γ ⊢ E_{2} ≅ E_{1} :C}
tra \frac{Γ ⊢ E_{1} ≅ E_{2} :C Γ ⊢ E_{2} ≅ E_{3} :C}{Γ ⊢ E_{1} ≅ E_{3} :C}  subI \frac{Γ, X:C ⊢ E_{1} ≅ E_{2} :D Γ′ ⊢ E:C}{Γ, Γ′ ⊢ E_{1}[E/X] ≅ E_{2}[E/X]:D}
appI \frac{Γ ⊢ F ≅ G:[C, D] Γ′ ⊢ E:C C small}{Γ, Γ′ ⊢ F (E) ≅ G(E):D}  lamI \frac{Γ, X:C ⊢ E_{1} ≅ E_{2} :D C small}{Γ ⊢ λX^{C}.E_{1} ≅ λX^{C}.E_{2} :[C, D]}

intI \frac{Γ, X:C^{op}, Y :C ⊢ E_{1} ≅ E_{2} :D C small D complete}{Γ ⊢ ∫_{X^{C^{op}} ,Y^{C}} E_{1} ≅ ∫_{X^{C^{op}} ,Y^{C}} E_{2} :D}

end \frac{Γ, X:C^{op}, Y :C ⊢ E:D C small D complete}{Γ, W:D^{op} ⊢ D(W, ∫_{X^{C^{op}} ,Y^{C}} E) ≅ ∫_{X^{C^{op}} ,Y^{C}} D(W, E):Set}

nat \frac{Γ, X:C ⊢ E_{1} :D Γ′, Y :C ⊢ E_{2} :D C small}{Γ^{op}, Γ′ ⊢ [C, D](λX^{C}.E_{1}, λY^{C}.E_{2}) ≅ ∫_{X^{C^{op}} ,Y^{C}} D(E_{1}, E_{2}):Set}

fub \frac{Γ, X:C^{op}, Y :C, W:D^{op}, Z:D ⊢ E:E C small D small E complete}{Γ ⊢ ∫_{X^{C^{op}} ,Y^{C}} ∫_{W^{D^{op}} ,Z^{D}} E ≅ ∫_{W^{D^{op}} ,Z^{D}} ∫_{X^{C^{op}} ,Y^{C}} E:E}

duaI \frac{Γ ⊢ E_{1} ≅ E_{2} :D}{Γ^{op} ⊢ E_{1}^{∗} ≅ E_{2}^{∗}:D^{op}}  opp\frac{Γ ⊢ E_{1} :C Γ′ ⊢ E_{2} :C}{Γ^{op}, Γ′ ⊢ C(E_{1}, E_{2}) ≅ C^{op}(E_{2}^{∗}, E_{1}^{∗}):Set}
uniI \frac{Γ ⊢ E:Set}{Γ ⊢ 1 × E ≅ E:Set}  com \frac{Γ ⊢ E_{1} :Set Γ′ ⊢ E_{2} :Set}{Γ, Γ′ ⊢ E_{1} × E_{2} ≅ E_{2} × E_{1} :Set}

clo \frac{Γ ⊢ E_{1} :Set Γ′ ⊢ E_{2} :Set Γ′′ ⊢ E_{3} :Set}{Γ^{op}, (Γ′)^{op}, Γ′′ ⊢ [E_{1} × E_{2}, E_{3}] ≅ [E_{1}, [E_{2}, E_{3}]]:Set}

yon \frac{Γ, X:C^{op} ⊢ E:Set C small}{Γ, Z:C^{op} ⊢ E[Z/X] ≅ [C^{op}, Set](λX^{C^{op}}.C(X, Z), λX^{C}.E):Set}

rep \frac{Γ, X:C^{op} ⊢ C(X, E_{1}) ≅ C(X, E_{2}):Set}{Γ ⊢ E_{1} ≅ E_{2} :C}X ∉ F V (E_{1}) ∪ F V (E_{2})

cur \frac{Γ, X:C, Y :D ⊢ E_{1} :E Γ′, X:C, Y :D ⊢ E_{2} :E C small D small}{Γ^{op}, Γ′ ⊢ [C × D, E](λX^{C}, Y^{D}.E_{1}, λX^{C}, Y^{D}.E_{2}) ≅ [C, [D, E]](λX^{C}.λY^{D}.E_{1}, λX^{C}.λY^{D}.E_{2}):Set}

Figure 3: Rules for natural isomorphisms. means in more informal mathematical notation that there is an isomorphism

E_{1}(X_{1}, ⋯, X_{n}, X) ≅^{θ_{X_{1},··· ,Xn,X}} E_{2}(X_{1}, ⋯, X_{n}, X)

natural in X_{1}, ⋯, X_{n}, X.

Thus we can abstract on the variable X to obtain an isomorphism

λX.E_{1}(X_{1}, ⋯, X_{n}, X) ≅^{⟨θ_{X_{1},··· ,Xn,X}⟩_{X}} λX.E_{2}(X_{1}, ⋯, X_{n}, X)

natural in X_{1}, ⋯, X_{n}. This justifies the conclusion of the rule (lamI). The rules for end, duality and application are interpreted in a similar way, their soundness resting on the earlier discussion. Just as we could derive the dual rule (end*) in § 3.5, we can derive dual rules (intI*), (rep*) and (fub*).

We can derive dual rules (intI*), (rep*) and (fub*) in a similar manner to the derivation of (end*).

The rules (clo) and (com) arise from the closed structure of Set. Notice that we abbreviate hom-expressions over Set by using brackets, e.g. [A, B] instead of Set(A, B). The “closed” structure of CAT gives the rule (cur) for currying. A rule for swapping arguments in functors is derivable from (cur), (nat) and (fub).

We can derive a rule for the covariant version of the Yoneda lemma. Take the small category ℂ in the premise of the rule (yon) to be an opposite category 𝔻^{op} to obtain:

Γ, Z:(𝔻^{op})^{op} ⊢ E[Z/X] ≅ [(𝔻^{op})^{op}, Set](λX^{(𝔻^{op})^{op}}.𝔻^{op}(X, Z), λX^{(𝔻^{op})^{op}}.E):Set

By applying (opp), (lamI) and (homI) (and rewriting) we get:

Γ, Z:𝔻 ⊢ E[Z/X] ≅ [𝔻, Set](λX^{𝔻}.𝔻(X, Z), λX^{𝔻}.E):Set.

5 Examples

5.1 Continuity

The two driving notions in the previous sections have been functoriality and natural isomorphism. The example below shows that the calculus is rich enough to prove continuity.

Definition 5.1 (Preservation of Limits) Let F : 𝕀 → C be a functor with limiting cone ⟨k_{I} : \underleftarrow{lim}_{𝕀} F → F (I)⟩_{I∈𝕀}, a functor G : C → D preserves the limit of F iff ⟨G(k_{I}) : G(\underleftarrow{lim}_{𝕀} F) → G(F (I))⟩_{I∈𝕀} is a limiting cone in D. Preservation of colimits is defined dually.

We say that G preserves 𝕀-index limits if G preserves the limits of all functors in [𝕀, C]. A functor which preserves all limits is called continuous.

One might expect to prove that a given functor preserves limits by showing an isomorphism of objects. This gives, however, a necessary but not sufficient condition.^{4} The situation improves when the isomorphism is sufficiently natural however:

Theorem 5.2 Assume that the categories C and D have limits for all functors with domain 𝕀. The functor G : C → D preserves 𝕀-indexed limits iff

\underleftarrow{lim}_{𝕀}(G ∘ F) ≅ G(\underleftarrow{lim}_{𝕀}F),

natural in F ∈ [𝕀, C] (see [6] for a proof.).

This theorem supplies the key to proving continuity within the calculus. For example, that C(C, X) preserves limits in X is a direct consequence of the naturality formula.

Another result we can prove in the calculus is that right adjoints preserve limits. Given the judgements

X:C ⊢ E_{1} :D and Y :D ⊢ E_{2} :C

respectively denoting functors E_{1} : C → D and E_{2} : D → C, an adjunction where, as functors, E_{1} is the left adjoint and E_{2} is the right adjoint consists of an isomorphism

X:C^{op}, Y :D ⊢ D(E_{1}, Y ) ≅ C(X, E_{2}):Set.

By Theorem 5.2 it is enough to prove

H:[𝕀, D] ⊢ E_{2}[∫_{I^{𝕀}} H/Y] ≅ ∫_{I^{𝕀}} E_{2}[H(I)/Y]:C

where ∫_{I^{𝕀}} H(I) is the limit of H. The proof proceeds backwards, using (rep) to obtain the goal:

C(X, E_{2}[∫_{I^{𝕀}} H(I)/Y]) ≅ C(X, ∫_{I^{𝕀}} E_{2}[H(I)/Y])

4There are examples of functors which preserve limiting objects but don’t preserve the limiting cones, see [3, ex. 5.3.16(4)].

The derivation of this goal is sketched in the chain of isomorphisms:

C(X, E_{2}[∫_{I^{𝕀}} H(I)/Y]) ≅ D(E_{1}, ∫_{I^{𝕀}} H(I))  by the adjunction,
≅ ∫_{I^{𝕀}} D(E_{1}, H(I))  by (end),
≅ ∫_{I^{𝕀}} C(X, E_{2}[H(I)/Y]) by the adjunction,
≅ C(X, ∫_{I^{𝕀}} E_{2}[H(I)/Y]) by (end).

We conclude that the functor denoted by Y :C ⊢ E_{2} :D preserves limits.

The dual result, i.e. left adjoints preserve colimits, follows from the rules opp and duaI. From the definition of adjunction and by applying the rule opp twice together with transitivity we get

X:C^{op}, Y :D ⊢ C^{op}(E_{2}^{∗}, X) ≅ D^{op}(Y, E_{1}^{∗}):Set

i.e. an adjunction where the functor denoted by E_{1}^{∗} is the right adjoint. From the derivation above we can conclude

H:[𝕀^{op}, C^{op}] ⊢ E_{1}^{∗}[∫_{I^{𝕀^{op}}} H(I)/X] ≅ ∫_{I^{𝕀^{op}}} E_{1}^{∗}[H(I)/X]:D^{op}

and by applying the rule duaI

H:[𝕀, C] ⊢ E_{1}[∫^{I^{𝕀}} H(I)/X] ≅ ∫^{I^{𝕀}} E_{1}[H(I)/X]:D.

5.2 Pointwise Limits

Assuming a complete category C and given a judgement

Γ, X:𝕀, Y :𝕁 ⊢ E:C

we can derive the expression

Γ ⊢ λY^{𝕁}. ∫_{X^{𝕀}} E ≅ ∫_{X^{𝕀}} λY^{𝕁}.E:[𝕁, C].  (5)

In other words, limits in functor categories are obtained pointwise.^{5} We first show

[𝕁, C](H, λY^{𝕁}. ∫_{X^{𝕀}} E) ≅ [𝕀, [𝕁, C]](λX^{𝕀}.H, λX^{𝕀}.λY^{𝕁}.E)

5That is provided the pointwise limits exist, but we assume C complete.

where H:[𝕁, C]^{op}. A derivation for this judgement is sketched in the following chain of isomorphisms:

[𝕁, C](H, λY^{𝕁}. ∫_{X^{𝕀}} E) ≅ ∫_{Y^{𝕁},Z^{𝕁^{op}}} C(H Z, ∫_{X^{𝕀}} E)  by (nat),
≅ ∫_{Y^{𝕁},Z^{𝕁^{op}}} ∫_{X^{𝕀}} C(H Z, E)  by (end),
≅ ∫_{X^{𝕀}} ∫_{Y^{𝕁},Z^{𝕁^{op}}} C(H Z, E)  by (fub),
≅ ∫_{X^{𝕀}}[𝕁, C](H, λY^{𝕁}.E)  by (nat),
≅ [𝕀, [𝕁, C]](λX.H, λX.λY.E) by (nat).

Now from the definition of limit (see § 3.4) we obtain

[𝕁, C](H, λY. ∫_{X^{𝕀}} E) ≅ [𝕁, C](H, ∫_{X^{𝕀}} λY.E)

and by (rep) we can conclude (5). From this and by using the rules (dua) and (duaI) we can derive the dual result: colimits in functor categories are obtained pointwise.

5.3 The Density Formula

Functor categories of the form [ℂ^{op}, Set] have a number of important properties that give them a special rank in the calculus.^{6} From the rules (yon) and (nat), a functor X:[ℂ^{op}, Set] is expressible as the end formula:

X(W) ≅ ∫_{Y^{ℂ^{op}}} [ℂ(Y^{−}, W), X(Y^{+})] .  (6)

There is also a coend formula for X, the so-called density formula:

X(W) ≅ ∫^{Y^{ℂ}} ℂ(W, Y^{+}) × X(Y^{−}) .  (7)

The chain of isomorphisms below sketches a derivation for this formula:

[ℂ^{op},Set](λW^{ℂ^{op}}. ∫^{Y^{ℂ}} ℂ(W, Y^{+}) × X(Y^{−}), Z)
≅ ∫_{W^{ℂ^{op}}}[(∫^{Y^{ℂ}} ℂ(W^{−}, Y^{+}) × X(Y^{−}), Z(W^{+})] by (nat),
≅ ∫_{W^{ℂ^{op}}} ∫_{Y^{ℂ^{op}}}[ℂ(W^{−}, Y^{+}) × X(Y^{−}), Z(W^{+})] by (end*) and (intI),
≅ ∫_{Y^{ℂ^{op}}} ∫_{W^{ℂ^{op}}}[ℂ(W^{−}, Y^{+}) × X(Y^{−}), Z(W^{+})] by (fub),
≅ ∫_{Y^{ℂ^{op}}} ∫_{W^{ℂ^{op}}} [X(Y^{−}), [ℂ(W^{−}, Y^{+}), Z(W^{+})]] by (com) and (clo)
≅ ∫_{Y^{ℂ^{op}}} [X(Y^{−}), ∫_{W^{ℂ^{op}}}[ℂ(W^{−}, Y^{+}), Z(W^{+})]] by (end) and (intI),
≅ ∫_{Y^{ℂ^{op}}}[X(Y^{−}), Z(Y^{+})]  by (6) and (intI),
≅ [ℂ^{op}, Set](X, Z)  by (nat).

6Such categories are called presheaf categories.

The next step applies the rule (rep*) to yield the isomorphism (7).

6 Implementation in Isabelle

As part of ongoing research we are carrying out the implementation of the calculus in the theorem prover Isabelle. The calculus is implemented in several user-defined theories which extend the initial theory Pure. Basically, Pure gives the built-in higher-order logic [14] on top of which we define the object-logic for categories.

There are two meta-level types: cat and exp for the types and the expressions of the language respectively. The types constructors are defined as constants, for example:

     Set    :: cat
     One    :: cat
     Op     :: cat => cat            ("_^op" [10] 10)
     FunCat :: [cat, cat] => cat     ("[_,_]") .

The syntax for the expressions is defined similarly, for example:

     Hom  :: [cat,exp,exp]=> exp
     Lam  :: (exp=>exp) => exp        (binder "LAM" 10)
     Into :: (exp=>exp) => exp        (binder "INTO" 10)
     Int  :: (exp=>exp) => exp        (binder "INT" 10) .

where Lam, Into and Int give the definition for the binders λ and ∫. There are two special constants to encode assertions for types and natural isomorphisms:

     ":"    :: [exp,cat] => o        (infixl 7)
     NatIso :: [exp,exp,cat] => o    ("_~_:_" [5,5,5] 5) .

The constant “:” takes a term and a type as input and returns a truth value, similarly NatIso takes two terms and a type a returns a truth value.

The judgements of the calculus correspond to theorems in the metalogic. For example, X : C^{op}, Y : C ⊢ C(X, Y) : Set is written in the object-logic for categories as

     !! X Y. [| X:C^op; Y:C |] ==> Hom(C,X,Y):Set .

Notice that the universal quantification prevents a possible instantiation of the meta-variables X and Y enforcing their treatment as variables in the object-logic level. The manipulation of the contexts in the rules is done through lifting. Thus, the definition of the rules is only concerned with the part of the context which changes. For example, the rule for typing end formulae is:

   int " ( !!X Y. [| X:C^op ; Y:C; C Small |] ==> E(X,Y):D)
                              ==> INTO X. INT Y. E(X,Y):D".

This approach gives the structural rules for free; the rule (ass) corresponds to a proof by assumption, exchange to rotating the assumptions in a subgoal, and so on. We are currently developing an alternative implementation of the calculus in Isabelle/HOL [12] where the contexts are defined explicitly as sets of pairs. This approach should ease the implementation of duality.

7 Conclusions, Related Work and Future Directions

A calculus which formalises an expressive fragment of category theory has been presented. The rules of the calculus support a calculational approach to universality where the manipulation of ends and coends plays a central role. We have shown how to formalise judgements about functoriality and how to verify isomorphisms. In this setting, we have explored duality and studied applications to encode and prove results on continuous functors. An implementation of the calculus in the theorem prover Isabelle has been outlined briefly.

Previous work in the automation of category theory has followed a somewhat different tack. Takeyama [18] presents a computer checked language with the goal of supplying a categorical framework for type theory and includes an implementation in the theorem prover Lego [16]. This follows in spirit the work of Rydeheard and Burstall [17] on formalising universal constructions in ML. Beylin and Dybjer [4] formalise monoidal categories and present a proof of the Mac Lane’s coherence theorem in Martin Löf’s type theory [13].

The interpretation of the rules suggests a language for natural isomorphisms. Observe that in theorem provers like Isabelle where a goal may contain unknowns, a witness for a natural isomorphism may be given as output of the proof search. More generally, a further extension to the calculus is to introduce expressions for natural transformations.

A richer language for types may be considered by adding new constructors like recursion and lifting. For recursive definition of categories we need to extend the language for types to allow expressions with variables. The lifted type C_{⊥} would be interpreted as the category C with an initial object ⊥ freely adjoined.

The utility of end and coend notation was demonstrated in the pioneering work of Kelly and others in enriched category theory [10]. In emphasising a calculus for categories, a goal has been to make working with functor categories routine. The formalisation here should lend itself to enriched category theory.

Acknowledgments: This work was inspired by Martin Hyland’s Cambridge part III lecture course on category theory and its emphasis on end and coend manipulation.

References

[1] A. Asperti and G. Longo. Categories, Types and Structures : An introduction to category theory for the working computer scientist. Foundations of Computing Series. MIT Press, 1991.

[2] H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2: Computational Structures. Oxford University Press, 1991.

[3] M. Barr and C. Wells. Category Theory for Computing Science. C.A.R. Hoare Series Editor. Prentice Hall, second edition, 1996.

[4] I. Beylin and P. Dybjer. Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. Lecture Notes in Computer Science, 1158, 1996.

[5] T. Braüner. An Axiomatic Approach to Adequacy. PhD thesis, BRICS PhD School, 1996.

[6] M. Cáccamo, J. M. E. Hyland, and G. Winskel. Lecture notes in category theory. Available from: www.brics.dk/˜ mcaccamo.

[7] G. L. Cattani. Presheaf Models for Concurrency. PhD thesis, BRICS PhD School, 1999.

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

[9] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation and open maps. In R. L. Constable, editor, Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, June 1993. IEEE Computer Society Press.

[10] G. M. Kelly. Basic Concepts of Enriched Category Theory, volume 64 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1982.

[11] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, second edition, 1998.

[12] T. Nipkow and L. Paulson. Isabelle HOL: The tutorial. Documentation included in the official distribution of Isabelle, Feb. 2001.

[13] B. Nordström, K. Petterson, and J. Smith. Programming in Martin-Löf’s Type Theory. An Introduction. Oxford University Press, 1990.

[14] L. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5(3):363–397, 1988.

[15] L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[16] R. Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, The University of Edinburgh, 1994.

[17] D. Rydeheard and R. Burstall. Computational Category Theory. International Series in Computer Science. Prentice Hall, 1988.

[18] M. Takeyama. Universal Structure and a Categorical Framework for Type Theory. PhD thesis, The University of Edinburgh, 1995.

Recent BRICS Report Series Publications

RS-01-27 Mario Jose Cáccamo and Glynn Winskel. A Higher-Order Calculus for Categories. June 2001. 24 pp. Appears in Boulton and Jackson, editors, Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs ’01 Proceedings, LNCS 2152, 2001, pages 136–153.

RS-01-26 Ulrik Frendrup and Jesper Nyholm Jensen. A Complete Axiomatization of Simulation for Regular CCS Expressions. June 2001. 18 pp.

RS-01-25 Bernd Grobauer. Cost Recurrences for DML Programs. June 2001. 51 pp. Extended version of a paper to appear in Leroy, editor, Proceedings of the 6th ACM SIGPLAN International Conference on Functional Programming, 2001.

RS-01-24 ZoltánÉsik and Zoltán L. Németh. Automata on Series-Parallel Biposets. June 2001. 15 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.

RS-01-23 Olivier Danvy and Lasse R. Nielsen. Defunctionalization at Work. June 2001. 45 pp. Extended version of an article to appear in Søndergaard, editor, 3rd International Conference on Principles and Practice of Declarative Programming, PPDP ’01 Proceedings, 2001.

RS-01-22 Zoltán Ésik. The Equational Theory of Fixed Points with Applications to Generalized Language Theory. June 2001. 21 pp. To appear in Kuich, editor, 5th International Conference, Developments in Language Theory DLT ’01 Proceedings, LNCS, 2001.

RS-01-21 Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. Equational Theories of Tropical Semirings. June 2001. 52 pp. Extended abstracts of parts of this paper have appeared in Honsell and Miculan, editors, Foundations of Software Science and Computation Structures, FoSSaCS ’01 Proceedings, LNCS 2030, 2000, pages 42–56 and in Gaubert and Loiseau, editors, Workshop on Max-plus Algebras and their Applications to Discrete-event Systems, Theoretical Computer Science, and Optimization, MAX-PLUS ’01 Proceedings, IFAC (International Federation of Automatic Control) IFAC Publications, 2001.