PUBLICATIONS DE L’INSTITUT MATHÉMATIQUE Nouvelle série, tome 64 (78), 1998, 21–35

DEDUCTIVE SYSTEMS AND CATEGORIES

Kosta Došen

Communicated by Žarko Mijajlović

Abstract. This is an attempt to motivate the introduction of the notions of deductive system (graph with identity arrows and composition) and category through identifying objects with sets of arrows having them as source or as target. Proof-theoretically, this means identifying a proposition with a set of deductions. The results reached here are related to two well-known representations in universal algebra and to the Yoneda Lemma.

In intuitionism one sometimes hears that a proposition should be identified with the collection of proofs for it, or deductions leading to it. This idea will here be considered in the context of categorial proof theory. At an abstract level, it will motivate the introduction of the notion of category, and a few related basic notions, as an instrument for talking about deductions.

For an introduction to categorial proof theory the reader may consult [3] (see also [1]). Let us only say that, in this theory, objects (of graphs, deductive systems and categories) should be taken as propositions, arrows as deductions, special arrows as axioms and operations on arrows as rules of inference.

Our topic is related to two well-known constructions in universal algebra: the Stone and Cayley representations. The proposition justifying the introduction of the notion of deductive system (Proposition 1) is related to an elementary aspect of the Stone representation of lattice orders, while the propositions justifying the introduction of the notion of category (Propositions 2 and 4) are generalizations and variants of the Cayley representation of monoids. This leads to a representation of every small category as a concrete category, i.e., a subcategory of the category of sets with functions (Proposition 3; see [2; §1.272]).

This last representation is related to the well-known representation in category theory due to Yoneda. However, the connection with the Yoneda Lemma, which introduces some complications whose relevance to proof theory is not immediately clear, will not be considered before the final part of the paper. It would be unwise to start immediately with more complex matters, which are not essential for our exposition, and might unnecessarily scare an uninformed reader.

AMS Subject Classification (1991): Primary 18A05, 18A10, 18A15

This paper will be at a very abstract level, as an introductory chapter of category theory. However, it will not go very far into this theory. The results it contains are not quite new, but we will present them in a new and, we hope, clearer way. In particular, their relevance to proof theory doesn’t seem to have been noted. These results will be very simple to prove once they have been formulated. As it happens often in category theory, the point is in the formulation, not in the proof. The simplicity and directness of the proof should be one more reason to believe that the notions in question are natural.

In the treatment adopted here, identifying a proposition with deductions where this proposition is a conclusion has no decisive primacy over identifying it with deductions where it is a premise. However, the former approach, which is also the one suggested by texts about intuitionism, is somewhat simpler to expose (it eschews a contravariance of the latter approach), and this is why we shall concentrate on it.

1. Graphs, deductive systems and categories. A graph consists of two sets, called the set of objects and the set of arrows, and two functions from arrows to objects, called the source and target functions. (We speak only of small graphs, and small categories later.) For objects of graphs we use the letters A, B, C,…, and for arrows f, g, h,…, with indices if needed. We write f : A ⊢ B to indicate that the source of the arrow f is A and its target B; we say that A ⊢ B is the type of f. For graphs we use the letters G, H,… A hom-set G(A, B) in a graph G is {f | f : A ⊢ B is an arrow of G}.

If X is the set of arrows and Y the set of objects, a graph may be defined as a function F from X to Y × Y. This function is obtained by pairing the source and target functions; so the source and target functions are recovered from F by composing with the first and second projection, respectively. A binary relation on Y may be identified with a graph F that is a one-one function. We can then forget about X, and consider just the image of F, i.e., a subset of Y × Y. If a binary relation is a set of ordered pairs, a graph is a family of ordered pairs indexed by the arrows, a family where the same ordered pair may occur several times with different indices. In other words, a graph is a multiset of ordered pairs.

Here is a watershed between proof theory and the rest of logic. Logicians are usually concerned with a consequence relation (if they are concerned with the business of consequence at all—there are so many things in logic), but proof theorists have to deal with a consequence graph, because there may be several different proofs with the same premise and the same conclusion.

A graph morphism F from a graph G to a graph H is a pair of functions, both written F, assigning respectively to every object A of G an object F (A) of H and to every arrow f : A ⊢ B of G an arrow F (f) : F (A) ⊢ F (B) of H. A graph morphism is an embedding iff it is one-one both on objects and on arrows, and it is an isomorphism iff it is a bijection both on objects and on arrows.

A graph G is a subgraph of a graph H iff there is a graph morphism F from G to H that is the inclusion function both on objects and on arrows. This means that the objects of G are included among the objects of H and the arrows of G among the arrows of H, and for every object A of G the object F (A) of H is A, while for every arrow F of G the arrow F (f) of H is f. Moreover, since F is a graph morphism, the arrows of G have in H the same sources and targets as in G.

For a graph G the graph G^{op} is obtained by taking the objects and arrows of G and making the source function of G the target function of G^{op} and the target function of G the source function of G^{op}.

An identity 1 in a graph G is a family of arrows 1_{A} : A ⊢ A of G, one for every object A of G. The members of an identity are called identity arrows. A composition ∘ in G is a function that to every pair (f : A ⊢ B, g : B ⊢ C) of arrows of G assigns an arrow g ∘ f : A ⊢ C of G. Note that a graph may or may not have an identity and a composition, and if it has them, they need not be unique.

A deductive system is a triple ⟨G, 1, ∘⟩ where G is a graph, 1 is an identity in G and ∘ is a composition in G. A functor F from a deductive system ⟨G, 1_{G}, ∘_{G}⟩ to a deductive system ⟨H, 1_{H}, ∘_{H}⟩ is a graph morphism from G to H that satisfies

F (1_{A}) = 1_{F (A)} (fun1) F (g ∘_{G} f) = F (g) ∘_{H} F (f). (fun2)

A deductive embedding is a functor that is an embedding, and a deductive isomorphism is a functor that is an isomorphism. (The graph morphism inverse to a deductive isomorphism must be a functor.) A deductive system ⟨G, 1_{G}, ∘_{G}⟩ is a subsystem of a deductive system ⟨H, 1_{H}, ∘_{H}⟩ iff G is a subgraph of H, the arrows in 1_{G} coincide with arrows in 1_{H} and ∘_{G} is the restriction of ∘_{H} to the arrows of G.

A deductive system ⟨G, 1, ∘⟩ is a category iff the following equalities hold between its arrows:

f ∘ 1_{A} = f (cat1right) 1_{B} ∘ f = f (cat1left) (h ∘ g) ∘ f = h ∘ (g ∘ f) (cat2)

A subcategory is a subsystem of a category.

2. Cone graphs. For every object A of a graph G let the left cone of A, denoted by V (A), be the set of arrows {g | (∃C)g : C ⊢ A is an arrow of G}. So V (A) is ⋃_{C} G(C, A). A function φ from V (A) to V (B) assigning to every arrow g : C ⊢ A of G an arrow φ(g) : C ⊢ B of G is called left-invariable (because the source of φ(g) is the same as the source of g).

The left-cone graph V (G) of a graph G is a graph whose objects are all the left cones of G and whose arrows are all the left-invariable functions between such cones. The source of such a left-invariable function is its domain and its target is the codomain.

The right cone of an object A of a G is {g | (∃C)g : A ⊢ C is an arrow of G}, which is equal to {g | (∃C)g : C ⊢ A is an arrow of G^{op}}, i.e., the left cone of A in G^{op}. The right-cone graph of G is the left-cone graph of G^{op}. (We shall not talk about right-cone graphs until section 6.)

Among the arrows of V (G) there is always an arrow I_{V (A)} : V (A) ⊢ V (A) that to every g in V (A) assigns g itself. So we always have an identity in V (G). For the arrows φ_{1} : V (A) ⊢ V (B) and φ_{2} : V (B) ⊢ V (D) of V (G) we define φ_{2} · φ_{1} : V (A) ⊢ V (D) as composition of functions; i.e., for every g : C ⊢ A in V (A)

(φ_{2} · φ_{1})(g) =^{def} φ_{2}(φ_{1}(g)).

So we always have a composition in V (G). It is clear that for every graph G the deductive system ⟨V (G), I, ·⟩ is a category. This category is a subcategory of the category of sets with functions.

3. From graphs to deductive systems. A graph morphism F from G to V (G) is called lifting iff for every object A of G we have that F (A) is V (A). A graph morphism G from V (G) to G is called grounding iff for every object V (A) of V (G) we have that G(V (A)) is A. Note that the function mapping every object A of G to V (A) is one-one, so that in a grounding graph morphism G(V (A)) stands for a unique A. Then we have the following proposition.

Proposition 1

1.1. G has a composition iff there is a lifting graph morphism from G to V (G). 1.2. G has an identity iff there is a grounding graph morphism from V (G) to

G.

Proof . 1.1. If G has a composition ∘, then we take that L(A) is V (A) and for an arrow f : A ⊢ B of G we define the arrow L_{f} : V (A) ⊢ V (B) of V (G), where L_{f} stands for L(f), by

L_{f}(g) =^{def} f ∘ g.

This defines a lifting graph morphism L. Conversely, if we have a lifting graph morphism F, then we define a composition ∘ in G by

f ∘ g =^{def} (F (f))(g)

(which, after replacing F by L, is exactly like the previous definition, only read in the other direction).

1.2. If G has an identity 1, then we take that G(V (A)) is A and for an arrow φ : V (A) ⊢ V (B) of V (G) we define the arrow G(φ) : A ⊢ B of G by

G(φ) =^{def} φ(1_{A}).

This defines a grounding graph morphism. (As L is a compositional lifting, so this is an identity grounding.) Conversely, if we have a grounding graph morphism G, then we define an identity 1 in G by

1_{A} =^{def} G(I_{V (A)}). □

Note that the proof of Proposition 1.1 would go through if V (A) were a homset G(C, A) for some fixed C, rather than a left cone, but the proof of Proposition 1.2 would then break down: we might be unable to define the grounding graph morphism of the left-to-right direction, since 1_{A} could fail to be in G(C, A) (restricting ourselves to G(A, A) would make undefinable the lifting graph morphism L of Proposition 1.1). Note also that the left-invariability of φ is essential for proving Proposition 1.2 from left to right: otherwise, we would not know that φ(1_{A}) is of the type A ⊢ B.

4. From deductive systems to categories. For ⟨G, 1, ∘⟩ a deductive system, consider the lifting graph morphism L from G to V (G) defined in the proof of Proposition 1.1. We call L the left compositional lifting of G. (Left compositional lifting maps the arrows X of G to partial operations from X to X; it is obtained by ”currying” the partial operation ∘ from X × X to X.) Then we can prove the following.

Lemma 1. The deductive system ⟨G, 1, ∘⟩ satisfies (cat1left) and (cat2) iff the left compositional lifting of G is a functor from ⟨G, 1, ∘⟩ to ⟨V (G), I, ·⟩.

Proof. We have

L_{1_{A}}(g) = 1_{A} ∘ g, by definition
I_{V (A)}(g) = g, by definition.

So if the right-hand sides of these two equalities are equal by (cat1left), then the left-hand sides are equal, too. Conversely, if the left-hand sides are equal by (fun1), then the right-hand sides are equal, too.

We also have

L_{f_{2}∘f_{1}}(g) = (f_{2} ∘ f_{1}) ∘ g, by definition
(L_{f_{2}} · L_{f_{1}})(g) = f_{2} ∘ (f_{1} ∘ g), by definition.

Then we reason exactly as above, using (cat2) and (fun2). □

Proposition 2. The deductive system ⟨G, 1, ∘⟩ is a category iff the left compositional lifting of G is a deductive embedding of ⟨G, 1, ∘⟩ into ⟨V (G), I, ·⟩.

Proof. Since L is one-one on objects, it will be an embedding iff it is one-one on arrows. Suppose ⟨G, 1, ∘⟩ satisfies (cat1right) and suppose L_{f_{1}} = L_{f_{2}}. Then we have

L_{f_{1}}(1_{A}) = L_{f_{2}}(1_{A}) ⇒ f_{1} ∘ 1_{A} = f_{2} ∘ 1_{A},  by definition
⇒ f_{1} = f_{2}, by (cat1right).

This, together with the left-to-right direction of Lemma 1, yields the proposition from left to right.

Suppose now L is a deductive embedding of ⟨G, 1, ∘⟩ into ⟨V (G), I, ·⟩. Hence it is also a functor, and by the right-to-left direction of Lemma 1, we have that ⟨G, 1, ∘⟩ satisfies (cat1left) and (cat2). It remains to show that it satisfies also (cat1right). For every arrow f : A ⊢ B of g and every arrow g in V (A) we have

(f ∘ 1_{A}) ∘ g = f ∘ (1_{A} ∘ g), by (cat2)
= f ∘ g,  by (cat1left).

So L_{f∘1_{A}} = L_{f}, and since L is one-one on arrows, f ∘ 1_{A} = f. □

Note that in the presence of (cat1left) and (cat2) we have that L_{f_{1}} = L_{f_{2}} iff L_{f_{1}}(1_{A}) = L_{f_{2}}(1_{A}). This is related to the fact that in the definition of category the equality (cat1right) can be replaced by the implication

f_{1} ∘ 1_{A} = f_{2} ∘ 1_{A} ⇒ f_{1} = f_{2}

provided we keep (cat1left) and (cat2). Similarly, (cat1left) can be replaced by the implication

1_{B} ∘ f_{1} = 1_{B} ∘ f_{2} ⇒ f_{1} = f_{2}

provided we keep (cat1right) and (cat2). And if we keep just (cat2), then we can replace both (cat1right) and (cat1left) by these two implications provided we add the equality 1_{A} ∘ 1_{A} = 1_{A}.

The right-to left direction of Proposition 2 can be proved simply by appealing to the fact that ⟨V (G), I, ·⟩ is a category and that a deductive system that can be deductively embedded into a category must be a category. (To check (cat1right), for example, we would have L_{f∘1_{A}} = L_{f} ·L_{1_{A}} = L_{f} ·I_{V (A)} = L_{f}·) Our proof, which is not more involved, has the advantage of separating the derivation of (cat1left) and (cat2), which does not depend on L being an embedding.

Anyway, this renders the right-to-left direction of Proposition 2 more trivial than the left-to-right direction. The latter direction saves this proposition from being mistaken for the following really trivial assertion:

A deductive system is a category iff there is a deductive embedding of it into a category.

Proposition 2 is about a particular deductive embedding and a particular category built out of the original deductive system.

Proposition 4 in section 6, which is related to Proposition 2, gives an alternative characterization of categories, which eschews the triviality of the right-to-left direction of Proposition 2.

5. The image of left compositional lifting. For ⟨G, 1, ∘⟩ a deductive system, an arrow φ : V (A) ⊢ V (B) of the left-cone graph V (G) will be called solidifiable iff for every g : C ⊢ A in V (A) we have

(solid)  φ(g) = φ(1_{A}) ∘ g.

This terminology is explained by imagining that the operation φ has been “solidified” in the arrow φ(1_{A}), which together with composition can serve to define φ. Solidifiable functions of V (G) should be interpreted in logic as rules of inference that, in the presence of composition, i.e., cut, can be replaced by axioms. As, for example, the conjunction-elimination rule

\frac{f : C ⊢ A ∧ B}{φ(f) : C ⊢ A}

can be replaced by φ(1_{A∧B}) : A ∧ B ⊢ A.

The following two assumptions are related to (solid):

(∃f)(∀g) φ(g) = L_{f}(g) (Lφ) φ(h ∘ g) = φ(h) ∘ g. (Mφ)

It is easy to see that (solid) always implies (Lφ), that (Lφ) implies (Mφ) in the presence of (cat2), and that (Mφ) implies (solid) in the presence of (cat1left). So in the presence of (cat1left) and (cat2) all these assumptions are equivalent. We also have that (solid) is equivalent to (Lφ) in the presence of (cat1right).

The subgraphs of V (G) with the same objects whose arrows φ satisfy respectively (solid), (Lφ) and (Mφ) will be denoted by SV (G), LV (G) and MV (G). The graph LV (G) is the image of the left compositional lifting of G.

We can prove the following lemmata concerning these graphs, Lemma 3 being a strengthening of Lemma 1 from left to right.

Lemma 2. For every deductive system ⟨G, 1, ∘⟩ we have that ⟨MV (G), I, ·⟩ is a subcategory of ⟨V (G), I, ·⟩.

Proof. We just have to check that (Mφ) holds when we substitute I_{V (A)} for φ, and that if (Mφ) holds for φ_{1} and φ_{2}, then it holds for φ_{2} · φ_{1}. □

Lemma 3. The deductive system ⟨G, 1, ∘⟩ satisfies (cat1left) and (cat2) iff the left compositional lifting of G is a functor from ⟨G, 1, ∘⟩ to the category ⟨SV (G), I, ·⟩.

Proof. If ⟨G, 1, ∘⟩ satisfies (cat1left) and (cat2), then (solid) is equivalent to (Mφ), i.e., the graphs SV (G) and MV (G) coincide, and by Lemma 2 we obtain that ⟨SV (G), I, ·⟩ is a category. In the presence of (cat1left) and (cat2), the graphs SV (G) and LV (G) coincide, too, and it remains to apply the left-to-right direction of Lemma 1 to obtain the lemma from left to right. The other direction of the lemma is an immediate consequence of the right-to-left direction of Lemma 1. □

Lemma 4. If the deductive system ⟨G, 1, ∘⟩ satisfies (cat1right), then the left compositional lifting of G is an isomorphism between the graphs G and SV (G).

Proof. Note first that in the presence of (cat1right) the graphs SV (G) and LV (G) coincide. We then define a graph morphism G from SV (G) to G by taking that G(V (A)) is A, and that for φ : V (A) ⊢ V (B) an arrow of SV (G) the arrow G(φ) : A ⊢ B of G is

G(φ) =^{def} φ(1_{A}).

This is the grounding graph morphism G of the proof of the left-to-right direction of Proposition 1.2 restricted to SV (G).

We then have that G(L_{f}) = f, since the left-hand side is f ∘1_{A}, by definition, and this is equal to F by (cat1right). We also have that L_{G(φ)} = φ, since L_{G(φ)}(g) is φ(1_{A}) ∘ g, by definition, and this is equal to φ(g) by (solid). □

Lemmata 3 and 4 yield the following version of Proposition 2 (whose rightto-left direction is again trivial).

Proposition 3. The deductive system ⟨G, 1, ∘⟩ is a category iff the left compositional lifting of G is a deductive isomorphism between ⟨G, 1, ∘⟩ and the category ⟨SV (G), I, ·⟩.

It follows that for a category ⟨G, 1, ∘⟩ the graph morphism G of the proof of Lemma 4, inverse to the isomorphism L, is a functor from ⟨SV (G), I, ·⟩ to ⟨G, 1, ∘⟩. When we want to check directly that G is a functor, we have that (fun1) is satisfied by definition, while for (fun2) we have to appeal to the solidifiability of φ_{2} to get

φ_{2}(φ_{1}(1_{A})) = φ_{2}(1_{A}) ∘ φ_{1}(1_{A}).

This indicates that the graph morphism G defined on the whole of V (G) need not be a functor from ⟨V (G), I, ·⟩ to ⟨G, 1, ∘⟩.

6. Left-cone and right-cone graphs. Analogous propositions, dual to those above, could be proved with right-cone graphs replacing left-cone graphs. There is not much interest in rehearsing what we obtained so far by turning things upside down. (The advantage of left lifting over right lifting is only that left lifting is covariant, whereas right lifting is contravariant.) However, it might be worth stating a consequence of Lemma 1 that combines left-cone and right-cone graphs.

Let ⟨G, 1, ∘⟩ be a deductive system and let f : A ⊢ B and g : B ⊢ C be arrows of G. So g ∘ f : A ⊢ C is an arrow of G. For the arrows f : B ⊢ A and g : C ⊢ B of G^{op} we define the arrow f ∘^{op} g : C ⊢ A of G^{op} to be the arrow g ∘ f : C ⊢ A of G^{op}. Then ∘^{op} is a composition in G^{op}, and since 1 is an identity in G^{op} as well as in G, we have that ⟨G^{op}, 1, ∘^{op}⟩ is a deductive system.

Proposition 4. The deductive system ⟨G, 1, ∘⟩ is a category iff (1) the left compositional lifting of G is a functor from ⟨G, 1, ∘⟩ to ⟨V (G), I, ·⟩ and (2) the left compositional lifting of G^{op} is a functor from ⟨G^{op}, 1, ∘^{op}⟩ to ⟨V (G^{op}), I, ·⟩.

Proof. If ⟨G, 1, ∘⟩ is a category, then ⟨G^{op}, 1, ∘^{op}⟩ is a category, too, and by the left-to-right direction of Lemma 1, we obtain (1) and (2).

Suppose now (1) and (2). Then, by the right-to-left direction of Lemma 1, it follows from (1) that (cat1left) holds in ⟨G, 1, ∘⟩, and from (2) that (cat1left) holds in ⟨G^{op}, 1, ∘^{op}⟩. But the arrow 1_{A} ∘^{op} f : B ⊢ A of G^{op} is the arrow f ∘ 1_{A} : A ⊢ B of G; so (cat1right) holds in ⟨G, 1, ∘⟩. That (cat2) holds in ⟨G, 1, ∘⟩ follows from the right-to-left direction of Lemma 1 and either (1) or (2). □

Note that in the proof of this proposition from right to left it is sufficient to assume either for the graph morphism of (1) or for the graph morphism of (2) that it satisfies (fun2): we need not assume that for both. But it follows from the proposition that if we assume (fun2) for one of these graph morphisms, then the other will satisfy (fun2), too.

The interest of Proposition 4 is that it gives an alternative characterization of categories without mentioning embedding into a category, as Proposition 2 does. The right-to-left direction of this proposition seems less trivial than the same direction of Proposition 2.

7. Definitions of deductive system and category in an alternative vocabulary. The notions of deductive system and category need not be defined in terms of a binary operation of composition: instead they can be defined in terms of two kinds of unary operation on arrows. Here are these alternative definitions.

A deductive system is now a quadruple ⟨G, 1, L, R⟩ where G is a graph and 1 is an identity in G, L is a function assigning to every arrow f : A ⊢ B of G a function L_{f} that maps arrows g : C ⊢ A of G to arrows L_{f}(g) : C ⊢ B of G, R is a function assigning to every arrow f : A ⊢ B of G a function R_{f} that maps arrows g : B ⊢ C of G to arrows R_{f}(g) : A ⊢ C of G,

and the following equality holds:

(L = R)  L_{f}(g) = R_{g}(f).

The notion of deductive system given by this definition is equivalent to the standard notion of section 1 by introducing ∘ in deductive systems ⟨G, 1, L, R⟩ by

(∘)  f ∘ g =^{def} L_{f}(g)

and by introducing L and R in deductive systems ⟨G, 1, ∘⟩ by

L_{f}(g) =^{def} f ∘ g (L)

R_{f}(g) =^{def} g ∘ f. (R)

This function L corresponds to left compositional lifting. It is obvious that in the new definition of deductive system we could omit either L or R, and define the omitted function in terms of the remaining one according to (L = R), but having both L and R enables us to state more clearly the new definition of category.

A category is now a deductive system ⟨G, 1, L, R⟩ where the following equalities hold:

L_{f}(1_{A}) = f (L1) R_{f}(1_{B}) = f (R1) R_{f}(L_{h}(g)) = L_{h}(R_{f}(g)). (LR)

Let us first note that (L = R) follows from these equalities, and hence need not be stipulated expressly:

L_{f}(g) = L_{f}(R_{g}(1_{A})),  by (R1)
= R_{g}(L_{f}(1_{A})), by (LR)
= R_{g}(f), by (L1).

Next we can show that the new notion of category is equivalent to the old one. If we define ∘ in a category ⟨G, 1, L, R⟩ by (∘), then it is quite easy to derive (cat1right), (cat1left) and (cat2). Conversely, if we define L and R in a category ⟨G, 1, ∘⟩ by (L) and (R), then it is as easy to derive (L1), (R1) and (LR). It remains to verify that if we start from a category ⟨G, 1, L, R⟩, introduce ∘ by (∘), and then in the resulting category ⟨G, 1, ∘⟩ introduce L and R by (L) and (R), we obtain again the original category ⟨G, 1, L, R⟩. And the same starting from ⟨G, 1, ∘⟩, and introducing first L and R by (L) and (R), and then ∘ by (∘). But all this is quite trivial.

We shall now show how the new definition of category is related to Proposition 4. This proposition amounts to asserting that for a deductive system ⟨G, 1, ∘⟩, with the definitions (L) and (R), the equalities

(L1)  L_{1_{A}}(g) = g,  (L2)  L_{f_{2}∘f_{1}}(g) = L_{f_{2}}(L_{f_{1}}(g))
(R1)  R_{1_{C}} (g) = g,  (R2)  R_{f_{1}∘f_{2}}(g) = R_{f_{2}}(R_{f_{1}}(g))

are interderivable with the equalities (cat1right), (cat1left) and (cat2). It is quite straightforward to show that, in the presence of (L) and (R), these four equalities are interderivable with (L1), (R1) and (LR). Actually, either (L2) or (R2) is superfluous. So by starting from a deductive system ⟨G, 1, L, R⟩, with (L = R), and by adding the equalities (L1) and (R1), together with (L2) or (R2) where ∘ has been eliminated according to (L) or (R), we obtain still another alternative definition of category in the vocabulary with L and R.

The characterization of categories of Proposition 2 doesn’t yield an equational formulation, in the style of a variety, as those suggested by Proposition 4, but a formulation in the style of a quasi-variety. We already mentioned such formulations in section 4. Without ∘, a category could be defined as a deductive system ⟨G, 1, L⟩ that satisfies the equalities (L1) and (L2), where f_{2}∘f_{1} is short for L_{f_{2}}(f_{1}), together with the implication

L_{f_{1}}(1_{A}) = L_{f_{2}}(1_{A}) ⇒ f_{1} = f_{2}.

There are other alternative formulations with R only, or both L and R, analogous to those mentioned in section 4.

8. Preorders and monoids. The notion of category is a common generalization of the notions of preorder (reflexive and transitive binary relation) and monoid (semigroup with identity). A preorder is a category whose graph is a binary relation (as explained in section 1). A monoid is a category with a single object. Consider the following two important statements tied respectively to preorders and monoids.

Stone Representation of Preorders. Consider a binary relation R ⊆ Y × Y. Then

1. R is transitive iff (∀A, B ∈ Y)((A, B) ∈ R ⇒ {C | (C, A) ∈ R} ⊆ {C | (C, B) ∈ R});

2. R is reflexive iff (∀A, B ∈ Y)({C | (C, A) ∈ R} ⊆ {C | (C, B) ∈ R} ⇒ (A, B) ∈ R).

Cayley Representation of Monoids. An algebra ⟨X, 1, ∘⟩ is a monoid iff the map assigning to every f in X the function L_{f} : g ↦ f ∘ g is a monomorphism from ⟨X, 1, ∘⟩ to the algebra ⟨X^{X}, I, ·⟩, where X^{X} is the set of all functions from X to X, the element I is the identity function on X and the operation · is composition of functions.

The first statement is of the same inspiration as Stone’s representation of distributive lattice orders in sets—it catches an elementary aspect of that representation. The second statement is best known in Cayley’s original version, where it applies to groups.

The Stone Representation of Preorders is a specialization of Proposition 1. By that proposition, a relation R is transitive, i.e., has a composition, iff there is a lifting graph morphism assigning to every pair (A, B) from R a left-invariable function from the left cone {(C, A) | (C, A) ∈ R} of A to the left cone {(C, B) | (C, B) ∈ R} of B. A relation R is reflexive, i.e., has an identity, iff there is a grounding graph morphism assigning to a left-invariable function from {(C, A) | (C, A) ∈ R} to {(C, B) | (C, B) ∈ R} the pair (A, B) from R. To pass to the Stone Representation we need only remark that there is a left-invariable function from {(C, A) | (C, A) ∈ R} to {(C, B) | (C, B) ∈ R} iff {C | (C, A) ∈ R} ⊆ {C | (C, B) ∈ R}.

Note that {C | (C, A) ∈ R} is not the left cone {(C, A) | (C, A) ∈ R} of A, and the function that maps the objects A to the sets {C | (C, A) ∈ R} need not be one-one. It is one-one if R is a partial order, i.e., R is also antisymmetric, which in the categorial context corresponds to the category being skeletal. The analogue of the Stone Representation for equivalence relations is the assertion that R ⊆ Y × Y is an equivalence relation iff

(∀A, B ∈ Y)((A, B) ∈ R ⇔ {C | (C, A) ∈ R} = {C | (C, B) ∈ R}).

Then the equality of the equivalence classes {C | (C, A) ∈ R} and {C | (C, B) ∈ R} is matched by a bijection between the left cones of A and B.

The Cayley Representation of Monoids is a specialization of Proposition 2. Now the left cone of the unique object of the monoid is simply the set of all arrows X of the monoid, and all functions from X to X are left-invariable (as well as rightinvariable). When the monoid is a group, the functions from X to X in the image of left compositional lifting are bijections. In the categorial context, this corresponds to there being for every arrow in a graph an arrow of the converse type. Such are the graphs of groupoids, i.e., categories where all arrows have inverses, with whom they compose to give identity arrows.

The specialization of Proposition 4 analogous to the Cayley Representation of Monoids reads as follows:

⟨X, 1, ∘⟩ is a monoid iff (1) the map assigning to every f in X the function L_{f} : g ↦ f ∘ g is a homomorphism from ⟨X, 1, ∘⟩ to ⟨X^{X}, I, ·⟩ and (2) the map assigning to every f in X the function R_{f} : g ↦ g ∘ f is a homomorphism from ⟨X, 1, ∘^{op}⟩ to ⟨X^{X}, I, ·⟩, where f ∘^{op} g =^{def} g ∘ f.

9. The Yoneda Lemma for deductive systems. We conclude this paper by considering briefly the connection between Proposition 3 and the Yoneda Lemma. Before stating a generalization of this lemma, adapted to the present context, we generalize the notion of natural transformation.

Let F and G be graph morphisms from a graph G to the graph H of a deductive system ⟨H, 1, ∘⟩. A natural transformation from G to F is a family t of arrows t_{A} : G(A) ⊢ F (A) of H, one for every object A of G, such that for every arrow f : A ⊢ B of G the following equality holds in ⟨H, 1, ∘⟩:

F_{f} ∘ t_{A} = t_{B} ∘ G_{f}

where F_{f} and G_{f} stand for F (f) and G(f), respectively.

Let ⟨S, I, ·⟩ be the category of sets with functions, and let S^{G} be the graph of the category whose objects are graph morphisms from G to S and whose arrows are natural transformations between these graph morphisms.

For ⟨G, 1, ∘⟩ a deductive system and C an object of G, consider the graph morphism L^{C} from G to S such that for every object A of G the object L^{C}(A) is the hom-set G(C, A) and for every arrow f : A ⊢ B of G the arrow L_{f}^{C} : G(C, A) ⊢ G(C, B), where L_{f}^{C} stands for L^{C}(f), is defined by

L_{f}^{C}(g) =^{def} f ∘ g.

The graph morphism L^{C} differs on objects from the left compositional lifting L of G: we now have hom-sets where we had left cones. Otherwise, on arrows, it is defined quite analogously.

By reproducing the usual proof of the Yoneda Lemma, one can then establish the following generalization of this lemma.

Yoneda Lemma. If F is a functor from the deductive system ⟨G, 1, ∘⟩ to ⟨S, I, ·⟩ and ⟨G, 1, ∘⟩ satisfies (cat1right), then for every object C of G there is a bijection between F (C) and the hom-set S^{G}(L^{C}, F).

Proof. For every element x of F (C), let the natural transformation t^{x} from L^{C} to F be defined by

t_{A}^{x}(g) =^{def} F_{g}(x)

where g ∈ G(C, A). That t^{x} is indeed a natural transformation is shown as follows:

F_{f}(t_{A}^{x}(g)) = F_{f}(F_{g}(x)), by definition
t_{B}^{x}(L_{f}^{C}(g)) = F_{f∘g}(x), by definition

and, since F is a functor, the right-hand sides are equal by (fun2).

For every natural transformation t in S^{G}(L^{C}, F), let the object G(t) of F (C) be defined by

G(t) =^{def} t_{C}(1_{C}).

First we check that G(t^{x}) = x:

G(t^{x}) = F_{1_{C}} (x),  by definition
= I_{F (C)}(x), by (fun1).

It remains to check that t^{G(t)} = t:

t_{A}^{G(t)}(g) = F_{g}(t_{C}(1_{C})),  by definition

= t_{A}(L_{g}^{C}(1_{C})), by t being a natural transformation = t_{A}(g), by definition and (cat1right). □

Note that we didn’t assume for this version of the Yoneda Lemma that L^{C} is a functor; otherwise, (cat1left) and (cat2) would have to hold for ⟨G, 1, ∘⟩. However, the proof is exactly as for the usual Yoneda Lemma, where ⟨G, 1, ∘⟩ is assumed to be a category. (One can also show, without (cat1left) and (cat2), that the bijection from F (C) to S^{G}(L^{C}, F) is natural in both C and F.)

This Yoneda Lemma, where ⟨G, 1, ∘⟩ satisfies only (cat1right), is related to Lemma 4, which relies on the same assumption for ⟨G, 1, ∘⟩. In particular, the definition of the grounding graph morphism G of the proof of Lemma 4 is quite analogous to the definition of the function G of the proof of the Yoneda Lemma.

The usual Yoneda Lemma has the following well-known corollary, which may also be deduced from the version above.

Corollary. If ⟨G, 1, ∘⟩ is a category, then for every object A and every object B of G there is a bijection between the hom-sets G(A, B) and S^{(G^{op})}(L^{A}, L^{B}).

Proof. If ⟨G, 1, ∘⟩ is a category, then ⟨G^{op}, 1, ∘^{op}⟩ is a category, too, and so by the Yoneda Lemma there is a bijection between S^{(G^{op})}(L^{A}, L^{B}) and L^{B}(A), which is by definition G^{op}(B, A), i.e., G(A, B). □.

This yields an embedding of G into S^{(G^{op})} with the Yoneda functor, which to A assigns L^{A} and to f : A ⊢ B assigns the natural transformation t^{f} defined by

t_{D}^{f}(g) =^{def} L_{g}^{B}(f) = g ∘^{op} f = f ∘ g

for g ∈ G^{op}(A, D) = G(D, A).

The Yoneda functor is parallel to the left compositional lifting L of G. Since by Proposition 3 the category ⟨G, 1, ∘⟩ is isomorphic to ⟨SV (G), I, ·⟩, we have an embedding of SV (G) into S^{(G^{op})}. This embedding is obtained by assigning to every left cone V (A) the functor L^{A} from G^{op} to S. On arrows, we first apply to a solidifiable left-invariable function φ : V (A) ⊢ V (B) the grounding graph morphism G of the proof of Lemma 4, which yields the arrow φ(1_{A}) : A ⊢ B of G; next, the Yoneda functor takes φ(1_{A}) to the natural transformation t^{φ(1_{A})}, such that t_{D}^{φ(1_{A})}(g), for g ∈ G(D, A) ⊆ V (A), is equal to φ(1_{A}) ∘ g. By (solid), this is φ(g). So the embedding of SV (G) into S^{(G^{op})} says that the solidifiable left-invariable functions of V (G) amount to natural transformations of S^{(G^{op})}.

Acknowledgement. I would like to thank Zoran Petrić for reading a draft of this paper. I would also like to thank the Mathematical Institute in Belgrade for inviting me to its Golden Jubilee Symposium.

References

[1] K. Došen, Deductive completeness, Bull. Symbolic Logic 2 (1996), 243–283 (Errata, ibid., p. 523).

[2] P.J. Freyd and A. Scedrov, Categories, Allegories, North- Holland, Amsterdam, 1990.

[3] J. Lambek and P.J. Scott, Introduction to Higher-Order Categorical Logic, Cambridge University Press, Cambridge, 1986.

Matematički institut (Received 25 06 1997) Kneza Mihaila 35 11001 Beograd, p.p. 367 Yugoslavia

IRIT, Université de Toulouse III 31062 Toulouse cedex France