Category Theory — a silly walk

Claus-Peter Wirth

Informatik 5, Universität Dortmund, D–44221, Germany

                       wirth@LS5.cs.uni-dortmund.de

June 12, 1993 Revised Rosenmontag, 1999 Revised 11.11 h, Nov. 11, 1999 Revised 11.11 h, Nov. 11, 2000 Preliminary version

Abstract: Being a syntax-oriented formalist I always had problems with the usual informal and graphical presentation of categories. This is my trial to overcome these problems.

This script was supported by my friend N. Bourbaki.

Contents

1 Basic Notions and Notations 1 2 Categories and Functors 2 3 Duality 7 4 On the Inside of Categories 8 5 Algebras 14 6 Co-Algebras 17 7 Di-Algebras 20 References 23

1 Basic Notions and Notations

‘N’ denotes the set of and ‘≺’ the ordering on natural numbers. We define N_{+} := { n ∈ N | 0 ≠ n }.

We use ‘⊎’ for the union of disjoint classes, ‘id’ for the identity function, and ‘V’ for the class of all sets (and urelements). For a class R we define domain, range, and restriction to and image and reverse-image of a class A by

\begin{aligned}dom(R) & := & \{ a | ∃b. (a, b) ∈ R \} & ; \\ ran(R) & := & \{ b | ∃a. (a, b) ∈ R \} & ; \\ _{A}↿R & := & \{ (a, b) ∈ R | a ∈ A \} & ; \\ ⟨A⟩R & := & \{ b | ∃a ∈ A. (a, b) ∈ R \} & ; \\ R⟨B⟩ & := & \{ a | ∃b ∈ B. (a, b) ∈ R \} & . \end{aligned}

For a class A we define its power class and the class of its non-empty finite subsets by

\begin{aligned}𝔓(A) & := & \{ B | B ⊆ A \} & ; \\ 𝔓_{N_{+}}(A) & := & \{ B | B ⊆ A ∧ |B| ∈ N_{+} \} & . \end{aligned}

For a (possibly) partial function B : V ⇝ 𝔓(V) and class^{1} A with A ⊆ dom(B) we define their product and co-product (or free sum) by

\begin{aligned}∏_{a∈A} B_{a} & := & \{ f : A → V | ∀a ∈ A. f(a) ∈ B_{a} \} & ; \\ ∐_{a∈A} B_{a} & := & \{ (a, b) ∈ A×V | b ∈ B_{a} \} & . \end{aligned}

1Note that the product is meaningless unless A is a set: If A is a proper class, then any function f with dom(f) = A is a proper class, so that the product will be the empty set.

2 Categories and Functors

The notion of an (abstract) category can reasonably be defined in several different ways. The following two are particularly useful. As prerequisites, define the morphism, domain, and codomain functions mor, Dom, Cod : V×V×V → V by ((h, s, t) ∈ V×V×V) mor(h, s, t) := h, Dom(h, s, t) := s, and Cod(h, s, t) := t.

Definition 2.1 (Category) A category C consists of (left indices deliberately omitted):

• a class _{C}Obj of objects,

• a class _{C}Arr of arrows with _{C}Arr ⊆ V×_{C}Obj×_{C}Obj,

• for each s ∈ Obj an identity _{C}Id_{s} with (Id_{s}, s, s) ∈_{C}Arr,

• a binary partial composition function _{C}⋄ : (_{C}Arr×_{C}Arr) ⇝ _{C}Arr with infix notation.

Now the following must hold:

1. dom( ⋄) = { (a, b) ∈ Arr×Arr | Cod(a) = Dom(b) }

2. ∀a, b ∈ Arr. ( Cod(a) = Dom(b) ⇒ ( \begin{matrix}& (a ⋄ b) ∈ Arr \\ ∧ & Dom(a ⋄ b) = Dom(a) \\ ∧ & Cod(a ⋄ b) = Cod(b) \end{matrix} ) )

3. ∀s ∈ Obj. ∀a ∈ Arr. \binom{( Dom(a) = s ⇒ (Id_{s}, s, s) ⋄ a = a )}{∧ ( Cod(a) = s ⇒ a ⋄ (Id_{s}, s, s) = a )}

4. ∀a, b, c ∈ Arr. ( \binom{Cod(a) = Dom(b)}{∧ Cod(b) = Dom(c)} ⇒ (a ⋄ b) ⋄ c = a ⋄ (b ⋄ c) )

Definition 2.2 (Category alternate) A category C consists of (left indices deliberately omitted):

• a class _{C}Obj of objects,

• for each (s, t) ∈ Obj×Obj a class _{C}Mor_{s,t} of morphisms,

• for each s ∈ Obj an identity _{C}Id_{s} with _{C}Id_{s} ∈_{C}Mor_{s,s},

• a binary partial composition function _{C}⋄ : (V×V) ⇝ V with infix notation.

Now the following must hold:

1. dom(⋄) = ⋃_{s,t,u∈Obj} Mor_{s,t} × Mor_{t,u}

2. ∀s, t, u ∈ Obj. ∀f ∈ Mor_{s,t}. ∀g ∈ Mor_{t,u}. (f ⋄ g) ∈ Mor_{s,u}

3. ∀s ∈ Obj. \binom{∀t ∈ Obj. ∀f ∈ Mor_{s,t}. Id_{s} ⋄ f = f}{∧ ∀r ∈ Obj. ∀g ∈ Mor_{r,s}. g ⋄ Id_{s} = g}

4. ∀s, t, u, v ∈ Obj. ∀f ∈ Mor_{s,t}. ∀g ∈ Mor_{t,u}. ∀h ∈ Mor_{u,v}. (f ⋄ g) ⋄ h = f ⋄ (g ⋄ h)

First consider C to be given according to Def. 2.1: We can define for s, t ∈ Obj:

Mor_{s,t} := { f | (f, s, t) ∈_{C}Arr }.

Now assume^{2} that the composition function depends only on the first component of the arrows but not on their domain and codomain, formally:

∀s, t, u, s′, t′, u′ ∈ Obj. ∀f, g, h. ( \begin{matrix}( & \begin{aligned}& (f, s, t), (f, s′, t′), (g, t, u), (g, t′, u′) ∈ Arr \\ ∧ & (f, s, t) ⋄ (g, t, u) = (h, s, u) \end{aligned} & ) \\ ⇒ (f, s′, t′) ⋄ (g, t′, u′) = (h, s′, u′) \end{matrix} ).

Note that this is always the case if

∀s, t, u, v ∈ Obj. \binom{Mor_{s,t} ∩ Mor_{u,v} = ∅}{∨ (s, t) = (u, v)}. (:§)

Under this assumption, the composition function on morphisms f, g can be defined just by adding any appropriate s, t, u such that (f, s, t), (g, t, u) ∈ Arr and taking the first component of the triple resulting from their composition.

Now the enumerated items of Def. 2.2 follow from the respective items of Def. 2.1.

Now, however, consider C to be given according to Def. 2.2: Then we can define

Arr := { (f, s, t) | f ∈ Mor_{s,t} ∧ s, t ∈ Obj }.

Again, the enumerated items of Def. 2.1 follow from the respective items of Def. 2.2. Moreover, if (§) holds, we can treat Dom and Cod as if they were directly defined on

Mor := ⋃_{s,t∈Obj} Mor_{s,t}

via^{3}

Dom(f) := ⋂_{∃t.f∈Mor_{s,t}} s ,  and  Cod(f) := ⋂_{∃s.f∈Mor_{s,t}} t .

All in all, if we have to define some concrete category, we can always choose the more convenient way and check the category property without translation. Moreover, by use of the translation given above, we can always use ‘Mor_{s,t}’, ‘Arr’, and ‘Mor’, no matter which way the category has been defined. In case of (§), we can even always use Dom and Cod and write the composition function on morphisms instead of arrows.

We will abbreviate “f ⋄ g” by “fg” and “f(gh)” (or “(fg)h”) by “fgh”. Moreover, when “fg” appears in any atomic formula A, this formula is to be replaced with the formula (A ∧ B), where B is a formula saying that the composition is defined, i.e. B is either Cod(f) = Dom(g) or ∃s, t, u ∈ Obj. (f ∈ Mor_{s,t} ∧ g ∈ Mor_{t,u}).

Finally we write

f::s→t

and intend it to mean any of either f ∈ Mor_{s,t} or (f, s, t) ∈ Arr.

2Even if this is not the case we could get a category in the sense of Def. 2.2 by setting Mor_{s,t} := { (f, s, t) | (f, s, t) ∈_{C}Arr }, thereby (together with the transformation in the other direction) establishing the equivalence of Def. 2.1 and Def. 2.2. We use the less general transformation because it is more useful in practice.

3Note that in a set theory with ur-elements, we need Hilbert’s ε-operator to define Dom(f) := εs. ∃t. f ∈ Mor_{s,t} &c.. Anyway, the simple meaning of this is: “Let Dom(f) be such that f ∈ Mor_{Dom(f),t}.”

Corollary 2.3 Let C be a category. Now Id_{s} is unique in Mor_{s,s} satisfying item (3) in Def. 2.1 or Def. 2.2. More precisely: For s ∈ Obj and i ∈ Mor_{s,s} with (i, s, s)(Id_{s}, s, s) = (Id_{s}, s, s) or (Id_{s}, s, s)(i, s, s) = (Id_{s}, s, s) we have i = Id_{s}.

Definition 2.4 (Functor) Let C, D be categories.

A (co-variant) functor F from C to D (written “F : C ↠ D”) is a triple

F = ((F_{Obj}, F_{Arr}), C, D)

or else

F = ((F_{Obj}, F_{Mor}), C, D)

with:

• An object function F_{Obj} : _{C}Obj → _{D}Obj. We abbreviate “F_{Obj}(s)” by “sF”.

• An arrow function F_{Arr} : _{C}Arr → _{D}Mor or else a morphism function F_{Mor} : _{C}Mor → _{D}Mor. We abbreviate “F_{Arr}(a)” by “_{a}F” and “F_{Mor}(f)” by “_{f}F”. Note that any morphism function F_{Mor} defines the corresponding arrow function F_{Arr} via F_{Arr}(f, s, t) := F_{Mor}(f), but the converse definition is not always possible.

Now for the array function (morphism function analogously) the following must hold:

1. ∀s, t ∈_{C}Obj. ∀f ∈_{C}Mor_{s,t}. (_{(f,s,t)}F, sF, tF) ∈ _{D}Arr.

2. ∀s ∈_{C}Obj. _{(_{C}Id_{s},s,s)}F = _{D}Id_{sF}.

3. ∀s, t, u ∈_{C}Obj. ∀f ∈_{C}Mor_{s,t}. ∀g ∈_{C}Mor_{t,u}.

(_{((f,s,t) _{C}⋄ (g,t,u))}F, sF, uF) = (_{(f,s,t)}F, sF, tF) _{D}⋄ (_{(g,t,u)}F, tF, uF) .

When C and D are given according to Def. 2.2 this reads:

1. ∀s, t ∈_{C}Obj. ∀f ∈_{C}Mor_{s,t}. _{f}F ∈ _{D}Mor_{sF,tF}.

2. ∀s ∈_{C}Obj. _{_{C}Id_{s}}F = _{D}Id_{sF}.

3. ∀s, t, u ∈_{C}Obj. ∀f ∈_{C}Mor_{s,t}. ∀g ∈_{C}Mor_{t,u}. _{(f _{C}⋄ g)}F =_{f}F _{D}⋄ _{g}F.

F is full if ∀s, t ∈_{C}Obj. ∀f′ ∈_{D}Mor_{sF,tF}. ∃f ∈_{C}Mor_{s,t}. _{(f,s,t)}F = f′. F is faithful if ∀s, t ∈_{C}Obj. ∀f, g ∈_{C}Mor_{s,t}. ( _{(f,s,t)}F = _{(g,s,t)}F ⇒ f = g ).

The identity functor 𝕀_{C} for C is the functor 𝕀_{C} := ((_{_{C}Obj}↿id,_{_{C}Mor}↿id), C, C) .

If ((_{_{C}Obj}↿id,_{_{C}Mor}↿id), C, D) is a functor, then it is called the inclusion functor from C to D and C is called a sub-category of D. If this functor is full, C is a full sub-category of D.

A contra-variant functor (or contra-functor) F from C to D (written “F : C ⇌ D”) differs from a co-variant functor only in the following (for F_{Arr} analogously):

1. ∀s, t ∈_{C}Obj. ∀f ∈_{C}Mor_{s,t}. _{f}F ∈ _{D}Mor_{tF,sF}.

3. ∀s, t, u ∈_{C}Obj. ∀f ∈_{C}Mor_{s,t}. ∀g ∈_{C}Mor_{t,u}. _{(f _{C}⋄ g)}F =_{g}F _{D}⋄ _{f}F Note that, due to our special notation for the application of F_{Arr} and F_{Mor}, we can get the references to C and D, resp., from the level and thus may omit them. E.g., we will write “_{Id_{s}}F = Id_{sF}” for “_{_{C}Id_{s}}F = _{D}Id_{sF}” as well as “_{(f ⋄ g)}F = _{f}F ⋄_{g}F” (or even “_{fg}F = _{f}F_{g}F”) for “_{(f _{C}⋄ g)}F = _{f}F _{D}⋄ _{g}F”.

Furthermore, note that ∀s, t ∈_{C}Obj. ∀f′ ∈_{D}Mor_{sF,tF}. ∃a ∈_{C}Arr. _{a}F = f′ does in general not imply that F is full, and that a faithful F does not have to satisfy ∀a, b ∈_{C}Arr. (_{a}F =_{b}F ⇒ a = b). This is one of the unusual cases in category theory where the domain and codomain information becomes crucial.

Definition 2.5 (Small, Large, and Superlarge) A category C is small if _{C}Arr is a set.^{4} It is large if it is not small. A superlarge category C is like a category, but where_{C}Obj and_{C}Arr are collections of classes.

Corollary 2.6 Let C and D be categories. If C and D are a small, then _{C}Obj, (_{C}Id_{s})_{s∈_{C}Obj}, _{C}⋄ , (_{C}Mor_{s,t})_{(s,t)∈_{C}Obj×_{C}Obj}, _{C}Arr, C, and all functors F : C ↠ D are sets. If C is large, then _{C}⋄ , _{C}Arr, C, and all functors F : C ↠ D are proper classes.

Example 2.7 (Categories of Sets)

The relation category of sets is the large category REL given as follows:

RELObj := 𝔓(V)
RELMor_{A,B} := { R | R ⊆ A×B } for A, B ∈ 𝔓(V).
R _{REL}⋄ S := R∘S for R, S ∈ _{REL}Mor.
RELId_{A} := _{A}↿id for A ∈ 𝔓(V).

The partial function category of sets is the large sub-category FUN of the category REL given by _{FUN}Obj := 𝔓(V) and for A, B ∈ 𝔓(V):

FUNMor_{A,B} := A ⇝ B := { f | f : A ⇝ B }

The (total function) category of sets is the large sub-category SET of the category FUN given by _{SET}Obj := 𝔓(V) and for A, B ∈ 𝔓(V):

SETMor_{A,B} := A → B := { f | f : A → B }

4This is, of course, equivalent to _{C}Obj and _{C}Mor_{s,t} being sets, for any s, t ∈ Obj.

Example 2.8 (Categories of Classes)

The relation category of classes is the superlarge category RELCLASS given as follows:

RELCLASSObj is the collection of all classes A ⊆ V.

RELCLASSMor_{A,B} is the collection all all classes R ⊆ A×B for A, B ⊆ V.

R _{RELCLASS}⋄ S := R∘S for R, S in _{RELCLASS}Mor.

RELCLASSId_{A} := _{A}↿id for A ⊆ V.

The (total function) category of classes is the superlarge sub-category CLASS of the superlarge category RELCLASS given by _{CLASS}Obj := _{RELCLASS}Obj and for A, B in _{RELCLASS}Obj:

CLASSMor_{A,B} is the collection of all f : A → B.

Example 2.9 (Category of 𝕊-Sorted Sets) Let 𝕊 be some set of sorts. The function category of 𝕊-sorted sets is the category SORT(𝕊) given as follows:

SORT(𝕊)Obj := 𝕊 → 𝔓(V) is the class of all 𝕊-sorted families of sets.

SORT(𝕊)Mor_{A,B} := { f : 𝕊 → (V ⇝ V) | ∀s ∈ 𝕊. f_{s} : A_{s} → B_{s} }

is the set of 𝕊-sorted functions from A to B for A, B ∈ _{SORT(𝕊)}Obj.

f _{SORT(𝕊)}⋄ g := (f_{s}∘g_{s})_{s∈𝕊} for f, g ∈ _{SORT(𝕊)}Mor.

SORT(𝕊)Id_{A} := (_{A_{s}}↿id)_{s∈𝕊} for A ∈ _{SORT(𝕊)}Obj.

Note that SORT(𝕊) is large iff 𝕊 ≠ ∅. Even in this case — although _{SORT(𝕊)}Obj and SORT(𝕊)Arr are proper classes — _{SORT(𝕊)}Mor_{A,B} is always a set because it is contained in the set 𝔓(⋃_{s∈𝕊} A_{s} × ⋃_{s∈𝕊} B_{s}).

Example 2.10 (Functor Categories of Categories)

The functor category of of small categories is the large category SMALL given as follows:

SMALLObj := { C | C is a category } is the proper class of all small categories. SMALLMor_{C,D} := { F | F : C ↠ D } is the set of all functors from

the small category C to the small category D.

(F_{Obj}, F_{Arr}) _{SMALL}⋄ (G_{Obj}, G_{Arr}) := (F_{Obj} ∘ G_{Obj}, H_{Arr}) where H_{Arr} is given by

(f,s,t)H := _{(_{(f,s,t)}F,sF,tF)}G for F : B ↠ C and F : C ↠ D.
SMALLId_{C} := 𝕀_{C}.

The functor category of of all categories is the superlarge category ALL given as follows:

ALLObj is the collection of all categories

— excluding the superlarge categories.

ALLMor_{C,D} is the collection of all functors F : C ↠ D from

the category C to the category D.

The rest is analogous to SMALL.

3 Duality

The duality principle is a very important tool for doing universal category theory because it halves the proof work. The principle is based on the cognition that things do not change when all arrows and their composition are reversed.

Definition 3.1 (Dual Category and Functor)

Let C be a category. The dual^{5} category of C is the category Dual(C) given by Dual(C)Obj := _{C}Obj; _{Dual(C)}Arr := { (f, t, s) | (f, s, t) ∈_{C}Arr }; _{Dual(C)}Id_{s} := _{C}Id_{s}; Dual(C)Mor_{s,t} := _{C}Mor_{t,s}; (g, u, t) _{Dual(C)}⋄ (f, t, s) := (f, s, t) _{C}⋄ (g, t, u).

Let F : C ↠ D. The dual functor of F

Dual(F) : Dual(C) ↠ Dual(D)

is given by Dual(F)_{Obj} := F_{Obj} and _{(f,t,s)}Dual(F) := _{(f,s,t)}F.

The dual contra-functor of F : C ↠ D is

F : C ⇌ Dual(D).

Of special interest is 𝕀_{C} : C ⇌ Dual(C), which in general is no co-variant functor because item (1) of Def. 2.4 is satisfied iff |_{C}Obj| ⪯ 1.

The dual expression of some expression ϕ is obtained by replacing each occurrence of a category or functor symbol X by Dual(X), reversing the arguments of all concatenations, replacing _{C}Mor_{s,t} with _{C}Mor_{t,s}, Dom with Cod, and Cod with Dom.

Simply speaking of the dual we mean what is obtained by substituting everything by its dual.

Note that the dual expression has the same truth value in the dual as the original expression in the original. Since Dual(Dual(C)) = C and Dual(Dual(F)) = F for F : C ↠ D, the dual of the dual is the original. Moreover, the dual of all categories and functors are all categories and functors: Indeed, the dual of the expression “C is a category” is logically equivalent to the expression “C is a category” itself. The same holds for the expression “F is a functor”. Since the dual of a logic inference is a logic inference, if a set of axioms A has a consequence ϕ, then the dual of ϕ is a consequence of the dual of A. Thus, the universal theory of categories and functors does not differ from its dual. Stated differently: If a general theorem about categories and functors is valid, then the dual theorem is valid, too. This “duality principle” is a very important tool for doing universal category theory because it halves the proof work.

5called opposite by some authors

4 On the Inside of Categories

In the whole section we assume C to be some category and omit the left indices to C.

Definition 4.1 t ∈ Obj is called … … initial if ∀u ∈ Obj. |Mor_{t,u}| = 1. … final (or terminal) if ∀s ∈ Obj. |Mor_{s,t}| = 1.

Thus, “final” is the dual of “initial”. … a zero object if t is initial and final.

Thus, “being a zero object” is the dual of itself.

E.g. in SET, ∅ is the only initial object, the terminal objects are exactly the sets with a single element, and zero objects do not exist.

Definition 4.2 a ∈ Arr is called … … monic if ∀b, c ∈ Arr. ( ba = ca ⇒ b = c ). … epi if ∀b, c ∈ Arr. ( ab = ac ⇒ b = c ).

Thus, “epi” is the dual of “monic”. … split-monic if ∃r ∈ Arr. ar = (Id_{Dom(a)}, Dom(a), Dom(a)).

Such an r is called a retraction of a. … split-epi if ∃l ∈ Arr. la = (Id_{Cod(a)}, Cod(a), Cod(a)).

Such an l is called a section of a.

Thus, “split-epi” and “section” are the dual of “split-monic” and “retraction”.

… iso if ∃a′ ∈ Arr. \binom{aa′ = (Id_{Dom(a)}, Dom(a), Dom(a))}{∧ a′a = (Id_{Cod(a)}, Cod(a), Cod(a))}.

Such an a′ is called the inversion of a. … endo if Dom(a) = Cod(a). … auto if a is iso and endo. … idempotent if aa = a.

Thus, “iso”, “endo”, “auto”, and “idempotent” are the duals of themselves. … an equalizer for p, q if ap = aq and ∀a′ ∈ Arr. ( a′p = a′q ⇒ ∃!c ∈ Arr. a′ = ca ). … a co-equalizer for p, q if pa = qa and ∀a′ ∈ Arr. ( pa′ = qa′ ⇒ ∃!c ∈ Arr. a′ = ac ).

Thus, “co-equalizer” is the dual of “equalizer”.

Definition 4.3

s, t ∈ Obj are called …

… isomorphic if ∃f ∈ Mor_{s,t}. ( (f, s, t) is iso ).

… uniquely isomorphic if ∃!f ∈ Mor_{s,t}. ( (f, s, t) is iso ).

Corollary 4.4 “isomorphic” and “uniquely isomorphic” are the duals of themselves.

Corollary 4.5 Let a ∈ Arr. a is iso iff a is split-monic and split-epi.

Lemma 4.6

(1) Two initial objects are uniquely isomorphic.
(2) An object isomorphic to an initial object is initial.
Dual(1) Two final objects are uniquely isomorphic.
Dual(2) An object isomorphic to an final object is final.

Proof of Lemma 4.6 \underline{(1):} Suppose that s, t are both initial. Define \{f\} := Mor_{s,t} and \{g\} := Mor_{t,s}. Now mor((f, s, t)(g, t, s)) ∈ Mor_{s,s} = {Id_{s}} and mor((g, t, s)(f, s, t)) ∈ Mor_{t,t} = {Id_{t}}.

Lemma 4.7

(1) If a is split-monic, then a is monic.
(2) If a is an equalizer for p, q, then a is monic.
Dual(1) If a is split-epi, then a is epi.
Dual(2) If a is a co-equalizer for p, q, then a is epi.

Proof of Lemma 4.7 \underline{(1):} For ba = ca we get b = b (Id_{Dom(a)}, Dom(a), Dom(a)) = bar = car = c (Id_{Dom(a)}, Dom(a), Dom(a)) = c. \underline{(2):} By the first property of an equalizer we get (ba)p = (ba)q for each b ∈ Arr with Cod(b) = Dom(a). Thus, (by the uniqueness part of the second property of an equalizer) ba = ca implies b = c.

Lemma 4.8 In the relation category^{6} REL of sets the following items are logically equivalent for R::A→B and C := { y | |R⟨{y}⟩| = 1 } :

1. R::A→B is split-monic.

2. R::A→B is monic.

3. ∀X, Y ⊆ A. ( ⟨X⟩R = ⟨Y ⟩R ⇒ X=Y ).

4. ∀x ∈ A. ⟨A⟩R ≠ ⟨A\{x}⟩R.

5. dom(R ∘_{C}↿id) = A.

6. R ∘_{C}↿id ∘ R^{−1} = _{A}↿id.

Proof of Lemma 4.8 \underline{(1) ⇒ (2):} By Lemma 4.7. \underline{(2) ⇒ (3):} Suppose ⟨X⟩R = ⟨Y ⟩R. Define S := \{∅\}×X and T := \{∅\}×Y. Then S∘R = {∅}×⟨X⟩R = {∅}×⟨Y ⟩R = T ∘R. Since R::A→B is monic, we get S = T, i.e. X = Y. \underline{(3) ⇒ (4):} If (4) were not true, (3) would imply A = A\\{x\} . \underline{(4) ⇒ (5):} “⊆” is trivial. For showing “⊇” assume x ∈ A but y ∉ C for all y with (x, y) ∈ R . Then we get ⟨A⟩R = ⟨A\{x}⟩R, which contradicts (4). \underline{(5) ⇒ (6):} “⊆” is true by definition of C. “⊇” follows from (5). \underline{(6) ⇒ (1):} We get _{C}↿id ∘ R^{−1}::B→A and R ∘_{C}↿id ∘ R^{−1} = _{A}↿id = _{REL}Id_{A}.

Lemma 4.9 In the relation category^{6} REL of sets the following items are logically equivalent for R::A→B and C := { y | |⟨{y}⟩R| = 1 } :

1. R::A→B is split-epi.

2. R::A→B is epi.

3. ∀X, Y ⊆ B. ( R⟨X⟩ = R⟨Y ⟩ ⇒ X = Y ).

4. ∀x ∈ B. R⟨B⟩ ≠ R⟨B\{x}⟩.

5. ran(_{C}↿id ∘ R) = B.

6. R^{−1} ∘_{C}↿id ∘ R = _{B}↿id.

Since Dual(REL) is isomorphic to REL via F : Dual(REL) ↠ REL given by AF := A and RF := R^{−1} and since Lemma 4.9 is the F-isomorphic of the dual of Lemma 4.8, we do not give a proof of Lemma 4.9 — even if the duality principle^{7} is actually only sufficient to infer the logical equivalence of (1) and (2).

6Cf. Ex. 2.7.

7Cf. Sect. 3.

Lemma 4.10 In the (total function) category^{8} SET of sets the following items are logically equivalent for f::A→B:

(1) f::A→B is an equalizer [for each p, q::B→C with ∀b ∈ B. ( p(b) = q(b) ⇔ b ∈ ran(f) )].

(2) f::A→B is monic.

(3) f : A → B is injective.

Furthermore, (1) - (3) are implied by

(4) f::A→B is split-monic.

In general, however, (4) is not implied by (1) - (3), but it is equivalent to

(5) f : A → B is injective and ( A = ∅ ⇒ B = ∅ ) .

Proof of Lemma 4.10 \underline{(1) ⇒ (2):} By Lemma 4.7. \underline{(2) ⇒ (3):} If f were not injective, there would be a, b ∈ dom(f) with a ≠ b and f(a) = f(b). Define g, h::{∅}→A by g(∅) := a and h(∅) := b. Thus, g ∘ f = h ∘ f and g ≠ h, which contradicts (2). \underline{(3) ⇒ (1):} For p, q as indicated, we get f ∘ p = f ∘ q. Furthermore, for f′::D→B with f′ ∘ p = f′ ∘ q we get ran(f′) ⊆ ran(f). Thus, since f is injective, we then can define h::D→A by h := f′∘f^{−1}, and get f′ = f′ ∘_{ran(f)}↿id = f′ ∘ f^{−1} ∘ f = h ∘ f. Finally, for any other h′::D→A with f′ = h′ ∘ f we get h′ = h′ ∘_{A}↿id = h′ ∘ f ∘ f^{−1} = f′ ∘ f^{−1} = h. \underline{(4) ⇒ (2):} By Lemma 4.7. \underline{(4) ⇒ (5):} If f has a retraction r::B→∅, we must have B = ∅. \underline{(5) ⇒ (4):} If A = ∅ = B, f has the retraction ∅::∅→∅. If there is some a ∈ A, f has the retraction r::B→A given by r(x) := f^{−1}(x) for x ∈ ran(f) and r(x) := a for x ∈ B\ran(f). \underline{In general not “(3) ⇒ (4)”:} Take f := A := ∅ and B := \{∅\} . Now f is injective but cannot have a retraction since _{SET}Mor_{B,∅} = ∅ .

8Cf. Ex. 2.7.

Lemma 4.11 In the (total function) category^{8} SET of sets the following items are logically equivalent for f::A→B:

(1) f::A→B is a co-equalizer [for p, q::C→A; C := ker(f) := f ∘ f^{−1}; and p, q given by ( (x, y) ∈ C) p(x, y) := x and q(x, y) := y ].

(2) f::A→B is epi.

(3) f : A → B is surjective (i.e. ran(f) = B).

Furthermore, (1) - (3) are implied by

(4) f::A→B is split-epi.

“(3) ⇒ (4)”, however, is equivalent to the set-version of (the function choice function version of) the Axiom of Choice.

Proof of Lemma 4.11 \underline{(1) ⇒ (2):} By Lemma 4.7. \underline{(2) ⇒ (3):} If ran(f) ≠ B, there would be some b ∈ B\ran(f). Define g, h::B→\{0, 1\} by g(b) := 1, g(x) := 0 for x ∈ B\{b}, and h(x) := 0 for x ∈ B. Thus, fg = fh and g ≠ h, which contradicts the assumption that f::A→B is epi. \underline{(3) ⇒ (1):} For p, q as indicated, we get p ∘ f = q ∘ f. Furthermore, for f′::A→D with p ∘ f′ = q ∘ f′ we get ker(f) ⊆ ker(f′) because f′ is total on A. Thus, since f : A → B is surjective, we then can define h::B→D by h := f^{−1}∘f′ and get f′ = f ∘f^{−1}∘f′ because of A↿id ⊆ f ∘f^{−1} ⊆ ker(f′). Thus f′ = f ∘h. Finally, for any other h′::B→D with f′ = f ∘h′, since f is surjective we get h′ = _{B}↿id ∘ h′ = _{ran(f)}↿id ∘ h′ = f^{−1} ∘ f ∘ h′ = f^{−1} ∘ f′ = h. \underline{(4) ⇒ (2):} By Lemma 4.7. \underline{Axiom of Choice, (3) ⇒ (4):} Since ran(f) = B, let f′′ : B → A be a function choice function of f′ : B → 𝔓(A) given by (x ∈ B) f′(x) := f⟨{x}⟩. Since f is a function and then by ran(f) = B we get f′′ ∘ f = _{ran(f)}↿id = _{B}↿id. Thus f′′::B→A is a section of f::A→B. \underline{((3) ⇒ (4)) ⇒ Axiom of Choice:} Assume g : B → 𝔓(V) with ∀x ∈ B. g(x) ≠ ∅. Define A := ⋃_{x∈B}({x}×g(x)) and the surjective f : A → B by f(x, y) := x . If this is supposed to imply that f::A→B is split-epi, then there must be a section f′::B→A of f::A→B. Define h : A → V by h(x, y) := y . Now f′ ∘ h is a function choice function of g. Indeed, for x ∈ B we get f(f′(x)) = x, f′(x) ∈ {x}× g(x), and h(f′(x)) ∈ g(x).

Lemma 4.12 In the partial function category^{9} FUN of sets the following items are logically equivalent for f::A→B:

(1) f::A→B is split-monic.

(2) f::A→B is monic.

(3) f : A ⇝ B is injective and dom(f) = A .

Proof of Lemma 4.12 \underline{(1) ⇒ (2):} By Lemma 4.7. \underline{(2) ⇒ (3):} If f were not total on A, there would be an a ∈ A\dom(f). Thus, _{\{a\}}↿id∘f = ∅∘f and _{{a}}↿id ≠ ∅, which contradicts (2) due to _{{a}}↿id::A→A and ∅::A→A. Thus, f::A→B is also in SET. Since SET is a sub-category of FUN and f::A→B is monic in FUN, f::A→B is also monic in SET. By Lemma 4.10, we conclude that f is injective. \underline{(3) ⇒ (1):} For injective f : A ⇝ B we get f^{−1}::B→A and f ∘ f^{−1} = _{dom(f)}↿id = _{A}↿id = FUNId_{A}.

Lemma 4.13 In the partial function category^{9} FUN of sets the following items are logically equivalent for f::A→B:

(1) f::A→B is epi.

(2) f : A ⇝ B is surjective (i.e. ran(f) = B).

Furthermore, (1) and (2) are implied by

(3) f::A→B is split-epi.

“ (1) ⇒ (3)”, however, is equivalent to the set-version of (the function choice function version of) the Axiom of Choice.

Proof of Lemma 4.13 \underline{(1) ⇒ (2):} If ran(f) ≠ B, there would be some b ∈ B\ran(f). Define g, h::B→\{0, 1\} by g(b) := 1, g(x) := 0 for x ∈ B\{b}, and h(x) := 0 for x ∈ B. Thus, f ∘ g = f ∘ h and g ≠ h, which contradicts the assumption that f::A→B is epi. \underline{(2) ⇒ (1):} Assume g, h::B→C with f ∘ g = f ∘ h. Since f is a function and then by (2) we get f^{−1} ∘f = _{ran(f)}↿id = _{B}↿id. Thus g = _{B}↿id∘g = f^{−1} ∘f ∘g = f^{−1} ∘f ∘h = _{B}↿id∘h = h. \underline{(3) ⇒ (1):} By Lemma 4.7. \underline{Logical equivalence with the Axiom of Choice:} The proof for this does not differ from the respective part of the proof of Lemma 4.11.

9Cf. Ex. 2.7.

5 Algebras

Definition 5.1 (Signature)

A signature (𝕊, 𝔽, rt) consists of

• a set of sorts 𝕊 and

• an 𝕊∗-sorted family 𝔽 = (𝔽_{s})_{s∈𝕊∗} of sets 𝔽_{s} of function symbols with argument sort s, and

• a result-type function rt : ∐_{s∈𝕊∗} 𝔽_{s} → 𝕊.

Example 5.2 (Signature)

Set 𝕊 := {1, zero, posnat, emptylist, nonemptylist, zero+posnat, zero+posnat+1, emptylist+nonemptylist}.

Note that 1 is included in 𝕊 in order to model the range of “undefined” function applications.

Set 𝔽_{∅} := {0, nil}; 𝔽_{zero} := {s}; 𝔽_{posnat} := {s, p};

𝔽_{emptylist} := {length}; 𝔽_{nonemptylist} := {length, car, cdr}; 𝔽_{zero zero} := 𝔽_{posnat zero} := 𝔽_{posnat posnat} := {+, –}; 𝔽_{zero posnat} :=

𝔽_{emptylist emptylist} := 𝔽_{emptylist nonemptylist} := 𝔽_{nonemptylist emptylist} := 𝔽_{nonemptylist nonemptylist} := {+}; 𝔽_{zero emptylist} := 𝔽_{zero nonemptylist} := 𝔽_{posnat emptylist} := 𝔽_{posnat nonemptylist} := {cons}; and 𝔽_{s} := ∅ for any other s ∈ 𝕊∗.

Set rt(∅, 0) := rt(emptylist, length) := rt(zero zero, +) := rt(zero zero, –) := zero; rt(zero, s) := rt(posnat, s) := rt(nonemptylist, length) := rt(zero posnat, +) :=

rt(posnat zero, +) := rt(posnat posnat, +) := rt(posnat zero, –) := posnat;

rt(posnat, p) := rt(nonemptylist, car) := zero+posnat; rt(posnat posnat, –) := zero+posnat+1; rt(∅, nil) := rt(emptylist emptylist, +) := emptylist; rt(emptylist nonemptylist, +) := rt(nonemptylist emptylist, +) :=

rt(nonemptylist nonemptylist, +) := rt(zero emptylist, cons) := rt(zero nonemptylist, cons) := rt(posnat emptylist, cons) :=

rt(posnat nonemptylist, cons) := nonemptylist; and

rt(nonemptylist, cdr) := emptylist+nonemptylist.

The following definition is classical.

Definition 5.3 ((𝕊, 𝔽, rt)-Algebra)

Let (𝕊, 𝔽, rt) be a signature.

A (total) (𝕊, 𝔽, rt)-algebra consists of

• a family A = (A_{s′})_{s′∈𝕊} of non-empty sets (“universes”) and,

• for each (s, f) ∈ ∐_{s∈𝕊∗} 𝔽_{s}, a function

(s, f)^{A} : ∏_{i≺ |s|} A_{s_{i}} → A_{rt(s,f)}.

Example 5.4

Let (𝕊, 𝔽, rt) be the signature of Ex. 5.2.

Set A_{1} := {ω}; A_{zero} := {0}; A_{posnat} := N_{+}; A_{emptylist} := {∅}; A_{nonemptylist} := N^{+}; and A_{zero+posnat} := A_{zero} ⊎A_{posnat}; A_{zero+posnat+1} := A_{zero+posnat} ⊎A_{1}; A_{emptylist+nonemptylist} := A_{emptylist} ⊎ A_{nonemptylist}.

For x, y ∈ N and k, l ∈ N∗ define:  (∅, 0)^{A}(∅) := 0;  (∅, nil)^{A}(∅) := ∅;

(zero, s)^{A}(x) := (posnat, s)^{A}(x) := x+1; (emptylist, length)^{A}(l) := (nonemptylist, length)^{A}(l) := |l|; (zero zero, +)^{A}(x, y) := (zero posnat, +)^{A}(x, y) :=

(posnat zero, +)^{A}(x, y) := (posnat posnat, +)^{A}(x, y) := x+y;

(posnat, p)^{A}(x+1) := (posnat zero, –)^{A}(x, 0) := (nonemptylist, car)^{A}(xl) := x; (posnat posnat, –)^{A}(x, y) := x−y for x ⪰ y; (posnat posnat, –)^{A}(x, y) := ω for x ≺ y; (emptylist emptylist, +)^{A}(k, l) := (emptylist nonemptylist, +)^{A}(k, l) :=

(nonemptylist emptylist, +)^{A}(k, l) := (nonemptylist nonemptylist, +)^{A}(k, l) := kl;

(zero emptylist, cons)^{A}(x, l) := (zero nonemptylist, cons)^{A}(x, l) :=

(posnat emptylist, cons)^{A}(x, l) := (posnat nonemptylist, cons)^{A}(x, l) := xl; and

(nonemptylist, cdr)^{A}(xl) := l .

Note that the signature of Ex. 5.2 is rather dull because s(p(s(s(0)))) is not a term although we can evaluate it: p(s(s(0))) has the sort zero+posnat and we have 𝔽_{zero+posnat} = ∅. Note that a signature cannot properly model functions with different range sorts for a single argument sort. This will be different with co-signatures in the next section.

While the notion of an algebra given in Def. 5.3 is nice, it is not very well suited for category theory. The first step for coming to the categorical definition of an algebra is to encode (𝕊, 𝔽, rt) into the following functor ((Σ_{Obj}, Σ_{Mor}), SORT(𝕊), SORT(𝕊)) from the category SORT(𝕊) of 𝕊-sorted sets^{10} into itself:

(AΣ)_{s′} := ∐_{(s,f)∈rt⟨{s′}⟩} ∏_{i≺ |s|} A_{s_{i}}

for A ∈_{SORT(𝕊)}Obj and s′ ∈ 𝕊, and

(_{h}Σ)_{s′}( (s, f), (a_{i})_{i≺ |s|} ) := ( (s, f), (h_{s_{i}}(a_{i}))_{i≺ |s|} )

for h::A→B in SORT(𝕊); s′ ∈ 𝕊; (s, f) ∈ rt⟨{s′}⟩; ∀i ≺ |s| . a_{i} ∈ A_{s_{i}}.

Now we can categorically represent the above algebra over (𝔽, 𝕊, rt) as the arrow (α, AΣ, A) ∈ _{SORT(𝕊)}Arr given by α_{s′}((s, f), a) := (s, f)^{A}(a) for ((s, f), a) ∈ (AΣ)_{s′}.

Definition 5.5 (Σ-Algebras and Σ-Homomorphisms) Let Σ : SORT(𝕊) ↠ SORT(𝕊). A Σ-algebra is an arrow (α, AΣ, A) ∈ _{SORT(𝕊)}Arr with ∀s ∈ 𝕊. A_{s} ≠ ∅. Let (α, AΣ, A) and (β, BΣ, B) be Σ-algebras. A Σ-homomorphism from (α, AΣ, A) to (β, BΣ, B) is a morphism h::A→B in SORT(𝕊) such that h is compatible with Σ in the sense that α _{SORT(𝕊)}⋄ h = _{h}Σ _{SORT(𝕊)}⋄ β.

AΣ \overline{_{_{_{h}Σ} >}} BΣ

=

A^{∨^{α}}  \overline{_{_{h} >}} B^{∨^{β}}

Note that for Σ defined from (𝕊, 𝔽, rt) as above, the latter condition means that for s′ ∈ 𝕊; (s, f) ∈ rt⟨{s′}⟩; ∀i ≺ |s| . a_{i} ∈ A_{s_{i}}:

h_{s′}( α_{s′}( (s, f), (a_{i})_{i≺ |s|} ) ) = β_{s′}( (s, f), (h_{s_{i}}(a_{i}))_{i≺ |s|} ),

i.e.

h_{s′}( (s, f)^{A}( (a_{i})_{i≺ |s|} ) ) = (s, f)^{B}( (h_{s_{i}}(a_{i}))_{i≺ |s|} ).

Definition 5.6 (ALG)

The Σ-homomorphism category ALG of Σ-algebras is given as follows:

ALGObj is the class of all Σ-algebras.

ALGMor_{(α,AΣ,A),(β,BΣ,B)} is the class of all Σ-homomorphisms h::A→B.

h _{ALG}⋄ k := h _{SORT(𝕊)}⋄ k

for h ∈ _{ALG}Mor_{(α,AΣ,A),(β,BΣ,B)} and h ∈ _{ALG}Mor_{(β,BΣ,B),(γ,CΣ,C)}.

ALGId_{(α,AΣ,A)} := _{SORT(𝕊)}Id_{A}.

Note that, while the morphisms of ALG are also morphisms of SORT(𝕊) and their composition is the same, ALG is no sub-category of SORT(𝕊) because the objects of ALG are no objects of SORT(𝕊).

10Cf. Ex. 2.9.

6 Co-Algebras

Definition 6.1 (Co-Signature)

A co-signature (𝕊, 𝔽, rt) consists of

• a set of sorts 𝕊 and

• an 𝕊-sorted family 𝔽 = (𝔽_{s})_{s∈𝕊} of sets 𝔽_{s} of function symbols with argument sort s, and

• a result-type function rt : ∐_{s∈𝕊}𝔽_{s} → 𝔓_{N_{+}}(𝕊).

Example 6.2 (Co-Signature)

Set 𝕊 := {1, zero, posnat, emptylist, nonemptylist} ∪P_{nat} ∪ P_{list} ∪ Q; P_{nat} := {zero×zero, zero×posnat, posnat×zero, posnat×posnat}; P_{list} := {emptylist×emptylist, emptylist×nonemptylist, nonemptylist×emptylist,

nonemptylist×nonemptylist}; and

Q := {zero×emptylist, zero×nonemptylist, posnat×emptylist, posnat×nonemptylist}.

Note that 1 is included in 𝕊 in order to model the domain of nullary functions and the range of “undefined” function applications.

Set 𝔽_{1} := {0, nil}; 𝔽_{zero} := {s}; 𝔽_{posnat} := {s, p};

𝔽_{emptylist} := {length}; 𝔽_{nonemptylist} := {length, car, cdr}; 𝔽zero ; × ; zero := 𝔽posnat ; × ; zero := 𝔽posnat ; × ; posnat := {+, –}; 𝔽zero ; × ; posnat := 𝔽_{s} := {+} for s ∈ P_{list}; and 𝔽_{s} := {cons} for s ∈ Q.

Set rt(1, 0) := rt(emptylist, length) := rt(zero ; × ; zero, +) := rt(zero ; × ; zero, –) := {zero}; rt(zero, s) := rt(posnat, s) := rt(nonemptylist, length) := rt(zero ; × ; posnat, +) :=

rt(posnat ; × ; zero, +) := rt(posnat ; × ; posnat, +) := rt(posnat ; × ; zero, –) := {posnat};

rt(posnat, p) := rt(nonemptylist, car) := {zero, posnat}; rt(posnat ; × ; posnat, –) := {1, zero, posnat}; rt(1, nil) := rt(emptylist ; × ; emptylist, +) := {emptylist}; rt(emptylist × nonemptylist, +) := rt(nonemptylist × emptylist, +) :=

rt(nonemptylist × nonemptylist, +) := rt(s, cons) := {nonemptylist} for s ∈ Q; and

rt(nonemptylist, cdr) := {emptylist, nonemptylist}.

Definition 6.3 ((𝕊, 𝔽, rt)-Co-Algebra)

Let (𝕊, 𝔽, rt) be a co-signature.

A (𝕊, 𝔽, rt)-co-algebra consists of

• a family A = (A_{s})_{s∈𝕊} of non-empty sets (“universes”) and,

• for each (s, f) ∈ ∐_{s∈𝕊} 𝔽_{s}, a function

(s, f)^{A} : A_{s} → ∐_{s′∈rt(s,f)} A_{s′}.

Example 6.4

Let (𝕊, 𝔽, rt) be the co-signature of Ex. 6.2.

Set A_{1} := {ω}; A_{zero} := {0}; A_{posnat} := N_{+}; A_{emptylist} := {∅}; A_{nonemptylist} := N^{+}; and A_{s×t} := A_{s} × A_{t} for s×t ∈ P_{nat} ∪ P_{list} ∪ Q.

For x, y ∈ N and k, l ∈ N∗ define:

(1, 0)^{A}(ω) := (posnat, p)^{A}(1) := (emptylist, length)^{A}(∅) := (zero ; × ; zero, +)^{A}(0, 0) :=

(zero ; × ; zero, –)^{A}(0, 0) := (posnat ; × ; posnat, –)^{A}(x, x) := (nonemptylist, car)^{A}(0l) := (zero, 0); (1, nil)^{A}(ω) := (emptylist ; × ; emptylist, +)^{A}(∅, ∅) := (nonemptylist, cdr)^{A}(x) := (emptylist, ∅); (zero, s)^{A}(x) := (posnat, s)^{A}(x) := (posnat, x+1); (nonemptylist, length)^{A}(l) := (posnat, |l|); (zero ; × ; posnat, +)^{A}(x, y) := (posnat ; × ; zero, +)^{A}(x, y) := (posnat ; × ; posnat, +)^{A}(x, y) :=

(posnat, x+y);

(posnat, p)^{A}(x+1) := (posnat ; × ; zero, –)^{A}(x, 0) := (nonemptylist, car)^{A}(xl) :=

(posnat, x) for x ∈ N_{+};

(posnat ; × ; posnat, –)^{A}(x, y) := (posnat, x−y) for x ≻ y; (posnat ; × ; posnat, –)^{A}(x, y) := (1, ω) for x ≺ y; (emptylist × nonemptylist, +)^{A}(k, l) := (nonemptylist × emptylist, +)^{A}(k, l) :=

(nonemptylist × nonemptylist, +)^{A}(k, l) := (nonemptylist, kl);

(s, cons)^{A}(x, l) := (nonemptylist, xl); and (nonemptylist, cdr)^{A}(xl) := (nonemptylist, l) for l ∈ N^{+}.

Note that the co-signature of Ex. 6.2 is rather dull because we cannot add three natural numbers: The co-signature does not know that the result of the first addition can be paired with a natural number in order to add it. Actually, we cannot even add two natural numbers, but the sorts in P_{nat} have hidden this. Note that a co-signature cannot contain pairing functions because they always need more than one argument.

While the notion of a co-algebra given in Def. 6.3 is nice, it is not very well suited for category theory. The first step for coming to the categorical definition of a co-algebra is to encode (𝕊, 𝔽, rt) into the following functor ((Δ_{Obj}, Δ_{Mor}), SORT(𝕊), SORT(𝕊)) from the category SORT(𝕊) of 𝕊-sorted sets^{11} into itself:

(AΔ)_{s} := ∏_{f∈𝔽_{s}}  ∐_{s′∈rt(s,f)} A_{s′}

for A ∈_{SORT(𝕊)}Obj and s ∈ 𝕊, and

(_{h}Δ)_{s}( (s′_{f}, a′_{f})_{f∈𝔽_{s}} ) := (s′_{f}, h_{s′_{f}} (a′_{f}))_{f∈𝔽_{s}}

for h::A→B in SORT(𝕊); s ∈ 𝕊; ∀f ∈ 𝔽_{s}. (s′_{f} ∈ rt(s, f) ∧ a′_{f} ∈ A_{s′_{f}}).

Now we can categorically represent the above co-algebra over (𝔽, 𝕊, rt) as the arrow (α, A, AΔ) ∈ _{SORT(𝕊)}Arr given by α_{s}(a)_{f} := (s, f)^{A}(a) for a ∈ A_{s} and f ∈ 𝔽_{s}.

Definition 6.5 (Δ-Co-Algebras and Δ-Co-Homomorphisms) Let Δ : SORT(𝕊) ↠ SORT(𝕊). A Δ-co-algebra is an arrow (α, A, AΔ) ∈ _{SORT(𝕊)}Arr with ∀s ∈ 𝕊. A_{s} ≠ ∅. Let (α, A, AΔ) and (β, B, BΔ) be Δ-co-algebras. A Δ-co-homomorphism from (α, A, AΔ) to (β, B, BΔ) is a morphism h::A→B in SORT(𝕊) such that h is compatible with Δ in the sense that α _{SORT(𝕊)}⋄ _{h}Δ = h _{SORT(𝕊)}⋄ β.

A  \overline{_{_{h} >}} B

=

AΔ^{∨^{α}}  \overline{_{_{_{h}Δ} >}} BΔ^{∨^{β}}

Note that for Δ defined from (𝕊, 𝔽, rt) as above, the latter condition means that for s ∈ 𝕊; f ∈ 𝔽_{s}; a ∈ A_{s}; and

for (s′, a′) := α_{s}(a)_{f}: ( s′, h_{s′}(a′) ) = β_{s}( h_{s}(a) )_{f},

i.e.

for (s′, a′) := (s, f)^{A}(a): ( s′, h_{s′}(a′) ) = (s, f)^{B}( h_{s}(a) ).

Definition 6.6 (COALG)

The Δ-co-homomorphism category COALG of Δ-co-algebras is given as follows:

COALGObj is the class of all Δ-co-algebras.

COALGMor_{(α,A,AΔ),(β,B,BΔ)} is the class of all Δ-co-homomorphisms h::A→B.

h _{COALG}⋄ k := h _{SORT(𝕊)}⋄ k

for h ∈ _{COALG}Mor_{(α,A,AΔ),(β,B,BΔ)} and h ∈ _{COALG}Mor_{(β,B,BΔ),(γ,C,CΔ)}.

COALGId_{(α,A,AΔ)} := _{SORT(𝕊)}Id_{A}.

Note that, while the morphisms of COALG are also morphisms of SORT(𝕊) and their composition is the same, COALG is no sub-category of SORT(𝕊) because the objects of COALG are no objects of SORT(𝕊).

11Cf. Ex. 2.9.

7 Di-Algebras

Definition 7.1 (Di-Signature)

A di-signature (𝕊, 𝔽, rt) consists of

• a set of sorts 𝕊 and

• an 𝕊∗-sorted family 𝔽 = (𝔽_{s})_{s∈𝕊∗} of sets 𝔽_{s} of function symbols with argument sort s, and

• a result-type function rt : ∐_{s∈𝕊∗} 𝔽_{s} → 𝔓_{N_{+}}(𝕊).

Example 7.2 (Di-Signature)

Set 𝕊 := {1, zero, posnat, emptylist, nonemptylist}.

Note that 1 is included in 𝕊 in order to model the range of “undefined” function applications.

Set 𝔽_{∅} := {0, nil}; 𝔽_{zero} := {s}; 𝔽_{posnat} := {s, p};

𝔽_{emptylist} := {length}; 𝔽_{nonemptylist} := {length, car, cdr}; 𝔽_{zero zero} := 𝔽_{posnat zero} := 𝔽_{posnat posnat} := {+, –}; 𝔽_{zero posnat} :=

𝔽_{emptylist emptylist} := 𝔽_{emptylist nonemptylist} := 𝔽_{nonemptylist emptylist} := 𝔽_{nonemptylist nonemptylist} := {+}; 𝔽_{zero emptylist} := 𝔽_{zero nonemptylist} := 𝔽_{posnat emptylist} := 𝔽_{posnat nonemptylist} := {cons}; and 𝔽_{s} := ∅ for any other s ∈ 𝕊∗.

Set rt(∅, 0) := rt(emptylist, length) := rt(zero zero, +) := rt(zero zero, –) := {zero}; rt(zero, s) := rt(posnat, s) := rt(nonemptylist, length) := rt(zero posnat, +) :=

rt(posnat zero, +) := rt(posnat posnat, +) := rt(posnat zero, –) := {posnat};

rt(posnat, p) := rt(nonemptylist, car) := {zero, posnat}; rt(posnat posnat, –) := {zero, posnat, 1}; rt(∅, nil) := rt(emptylist emptylist, +) := {emptylist}; rt(emptylist nonemptylist, +) := rt(nonemptylist emptylist, +) :=

rt(nonemptylist nonemptylist, +) := rt(zero emptylist, cons) := rt(zero nonemptylist, cons) := rt(posnat emptylist, cons) :=

rt(posnat nonemptylist, cons) := {nonemptylist}; and

rt(nonemptylist, cdr) := {emptylist, nonemptylist}.

Definition 7.3 ((𝕊, 𝔽, rt)-Di-Algebra)

Let (𝕊, 𝔽, rt) be a di-signature.

A (𝕊, 𝔽, rt)-di-algebra consists of • a family A = (A_{s})_{s∈𝕊} of non-empty sets (“universes”) and,

• for each (s, f) ∈ ∐_{s∈𝕊} 𝔽_{s}, a function

(s, f)^{A} : ∏_{i≺ |s|} A_{s_{i}} → ∐_{s′∈rt(s,f)} A_{s′}.

Example 7.4

Let (𝕊, 𝔽, rt) be the di-signature of Ex. 7.2.

Set A_{1} := {ω}; A_{zero} := {0}; A_{posnat} := N_{+}; A_{emptylist} := {∅}; A_{nonemptylist} := N^{+}.

For x, y ∈ N and k, l ∈ N∗ define:

(∅, 0)^{A}(ω) := (posnat, p)^{A}(1) := (emptylist, length)^{A}(∅) := (zero zero, +)^{A}(0, 0) :=

(zero zero, –)^{A}(0, 0) := (posnat posnat, –)^{A}(x, x) := (nonemptylist, car)^{A}(0l) := (zero, 0); (∅, nil)^{A}(ω) := (emptylist emptylist, +)^{A}(∅, ∅) := (nonemptylist, cdr)^{A}(x) := (emptylist, ∅); (zero, s)^{A}(x) := (posnat, s)^{A}(x) := (posnat, x+1); (nonemptylist, length)^{A}(l) := (posnat, |l|); (zero posnat, +)^{A}(x, y) := (posnat zero, +)^{A}(x, y) := (posnat posnat, +)^{A}(x, y) :=

(posnat, x+y);

(posnat, p)^{A}(x+1) := (posnat zero, –)^{A}(x, 0) := (nonemptylist, car)^{A}(xl) :=

(posnat, x) for x ∈ N_{+};

(posnat posnat, –)^{A}(x, y) := (posnat, x−y) for x ≻ y; (posnat posnat, –)^{A}(x, y) := (1, ω) for x ≺ y; (emptylist nonemptylist, +)^{A}(k, l) := (nonemptylist emptylist, +)^{A}(k, l) :=

(nonemptylist nonemptylist, +)^{A}(k, l) := (nonemptylist, kl);

(s, cons)^{A}(x, l) := (nonemptylist, xl); and (nonemptylist, cdr)^{A}(xl) := (nonemptylist, l) for l ∈ N^{+}.

Note that the di-signature of Ex. 7.2 is rather fine because the problems with the cosignature of Ex. 6.2 and the problems with the signature of Ex. 5.2 are both overcome. On the one hand, we can now add three natural numbers: The di-signature does know that the result of the first addition can be paired with a natural number in order to add it. On the other hand, s(p(s(s(0)))) is a term w.r.t. the di-algebra of Ex. 7.4 because p(s(s(0))) has the sort posnat. Note, however, that in order to tell whether s(p(s(s(0)))) really denotes something we have to know to which specific di-algebra the question refers. The di-signature must accept s(p(s(s(0)))) as a term without knowing whether it denotes something. This problem of di-signatures already exists for co-signatures.

While the notion of a di-algebra given in Def. 7.3 is nice, it is not very well suited for category theory. The first step for coming to the categorical definition of a di-algebra is to encode (𝕊, 𝔽, rt) into the following two functors ((Γ_{Obj}, Γ_{Mor}), SORT(𝕊), SORT(𝕊∗)) and ((Δ_{Obj}, Δ_{Mor}), SORT(𝕊), SORT(𝕊∗)) from the category SORT(𝕊) of 𝕊-sorted sets into the category SORT(𝕊∗) of 𝕊∗-sorted sets:

(AΓ)_{s} := ∏_{i≺ |s|} A_{s_{i}}

(AΔ)_{s} := ∏_{f∈𝔽_{s}}  ∐_{s′∈rt(s,f)} A_{s′}
(_{h}Γ)_{s}( (a_{i})_{i≺ |s|} ) := (h_{s_{i}}(a_{i}))_{i≺ |s|}
(_{h}Δ)_{s}( (s′_{f}, a′_{f})_{f∈𝔽_{s}} ) := (s′_{f}, h_{s′_{f}} (a′_{f}))_{f∈𝔽_{s}}

for A ∈_{SORT(𝕊)}Obj; h::A→B in SORT(𝕊); s ∈ 𝕊∗, ∀i ≺ |s| . a_{i} ∈ A_{s_{i}}; and ∀f ∈ 𝔽_{s}. (s′_{f} ∈ rt(s, f) ∧ a′_{f} ∈ A_{s′_{f}}).

Now we can categorically represent the above di-algebra over (𝔽, 𝕊, rt) using the morphism α::AΓ→AΔ in SORT(𝕊∗) given by α_{s}(a)_{f} := (s, f)^{A}(a) for a ∈ A_{s} and f ∈ 𝔽_{s}.

While the definition of a Σ-algebra is standard and the definition of a Γ-co-algebra is its dual, the definition of a (Γ, Δ)-di-algebra below is our invention.

Definition 7.5 ((Γ, Δ)-Di-Algebras and (Γ, Δ)-Di-Homomorphisms) (Cf. Fokkinga (1996).) Let Γ, Δ : SORT(𝕊) ↠ SORT(𝕊∗). A (Γ, Δ)-di-algebra is a pair (A, α) with A ∈_{SORT(𝕊)}Obj; ∀s ∈ 𝕊. A_{s} ≠ ∅; and α::AΓ→AΔ in SORT(𝕊∗). Let (A, α) and (B, β) be (Γ, Δ)-di-algebras. A (Γ, Δ)-di-homomorphism from (A, α) to (B, β) is a morphism h::A→B in SORT(𝕊) such that h is compatible with (Γ, Δ) in the sense that α _{SORT(𝕊∗)}⋄ _{h}Δ = _{h}Γ _{SORT(𝕊∗)}⋄ β.

AΓ \overline{_{_{_{h}Γ} >}} BΓ

=

AΔ^{∨^{α}}  \overline{_{_{_{h}Δ} >}} BΔ^{∨^{β}}

Note that for (Γ, Δ) defined from (𝕊, 𝔽, rt) as above, the latter condition means that for s ∈ 𝕊∗; f ∈ 𝔽_{s}; ∀i ≺ |s| . a_{i} ∈ A_{s_{i}}; and

for (s′, a′) := α_{s}( (a_{i})_{i≺ |s|} )_{f}: ( s′, h_{s′}(a′) ) = β_{s}( (h_{s_{i}}(a)_{i})_{i≺ |s|} )_{f},

i.e.

for (s′, a′) := (s, f)^{A}( (a_{i})_{i≺ |s|} ): ( s′, h_{s′}(a′) ) = (s, f)^{B}( (h_{s_{i}}(a_{i}))_{i≺ |s|} ).

Definition 7.6 (SUALG)

The (Γ, Δ)-di-homomorphism category SUALG of (Γ, Δ)-di-algebras is given as follows:

SUALGObj is the class of all (Γ, Δ)-di-algebras.

SUALGMor_{(A,α),(B,β)} is the class of all (Γ, Δ)-di-homomorphisms h::A→B.

h _{SUALG}⋄ k := h _{SORT(𝕊)}⋄ k for h ∈ _{SUALG}Mor_{(A,α),(B,β)} and h ∈ _{SUALG}Mor_{(B,β),(C,γ)}.

SUALGId_{(A,α)} := _{SORT(𝕊)}Id_{A}.

Note that, while the morphisms of SUALG are also morphisms of SORT(𝕊) and their composition is the same, SUALG is no sub-category of SORT(𝕊) because the objects of SUALG are no objects of SORT(𝕊).

References

Maarten M. Fokkinga (1996). Datatype Lawes without Signatures. Math. Struct. in Comp. Sci. 6, pp. 1-32, Cambridge Univ. Press.