Category Theory

Claus-Peter Wirth

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

wirth@LS5.cs.uni-dortmund.de

June 12, 1993 Revised Rosenmontag, 1999

Preliminary version

Abstract:

This research was supported by my friend N. Bourbaki

Contents

1 Basic Notions and Notations 1 2 Basic Examples 5 3 Duality 6 4 On the Inside of Categories 7 5 Algebras 12 References ??

1 Basic Notions and Notations

Definition 1.1 (Category) A category C (also called an abstract category) consists of (left indices deliberately omitted):

• a class _{C}Obj of objects,

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

• a binary partial composition function _{C}⋄ with infix notation, and either

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

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

with: 1. ∀s ∈ Obj: Id_{s} ∈ Mor_{s,s}

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

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

4. ∀s, t ∈ Obj: ∀f ∈ Mor_{s,t}: Id_{s} ⋄ f = f = f ⋄ Id_{t}

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

6. C is called a small category if _{C}Obj and _{C}Mor_{s,t} are sets, for any s, t ∈ Obj. or

• a class _{C}Arr of arrows (or morphisms),

• a domain function _{C}Dom: Arr → Obj,

• a codomain function _{C}Cod: Arr → Obj, with:

1. ∀s ∈ Obj: ( Id_{s} ∈ Arr ∧ Dom(Id_{s}) = s = Cod(Id_{s}) )

2. dom( ⋄) = { (f, g) ∈ Arr×Arr | Cod(f) = Dom(g) }

3. ∀f, g ∈ Arr: ( Cod(f) = Dom(g) ⇒ ( \begin{matrix}& (f ⋄ g) ∈ Arr \\ ∧ & Dom(f ⋄ g) = Dom(f) \\ ∧ & Cod(f ⋄ g) = Cod(g) \end{matrix} ) )

4. ∀f ∈ Arr: Id_{Dom(f)} ⋄ f = f = f ⋄ Id_{Cod(f)}

5. ∀f, g, h ∈ Arr: ( \binom{Cod(f) = Dom(g)}{∧ Cod(g) = Dom(h)} ⇒ (f ⋄ g) ⋄ h = f ⋄ (g ⋄ h) )

6. C is called a small category if _{C}Arr is a set.

First consider the definition of C to be given according to the “either”-case: Then (§) allows to define Arr and Dom, Cod: Arr → Obj by (f ∈ Arr):

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

Now the items of the “or”-case follow from the respective items of the “either”-case.

Now consider the definition of C to be given according to the “or”-case: Then we define for s, t ∈ Obj:

Mor_{s,t} := { f ∈ Arr | (Dom(f), Cod(f)) = (s, t) } .

Now the items of the “either”-case follow from the respective items of the “or”-case. Note, that if _{C}Arr is a set, then { _{C}Id_{s} | s ∈_{C}Obj } is a set, and by the function _{C}Dom and the Axiom of Replacement _{C}Obj is a set, too.

All in all, both ways of defining a category are completely equivalent. Thus, 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 together with Arr, Dom, and Cod for dealing with a single certain category, no matter which way it has been defined.

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 ∧ Cod(f) = Dom(g) ).

For many categories, (§) must be achieved in a rather artificial way: Instead of defining Mor_{s,t} by Mor_{domain-object,codomain-object} := { f | P (f) } one has to define it more clumsily by

Mor_{domain-object,codomain-object} := { (f, domain-object, codomain-object) | P (f) } .

This, however, forces us to read and write lots of formulas of the form

“ (f, domain-object, codomain-object) ∈ Mor_{domain-object,codomain-object} ”,

which may be very tiresome. Instead, we prefer to write

“ f::domain-object→codomain-object ”

and intend it to mean “ f ∈ Mor_{domain-object,codomain-object} ” unless (§) requires it to mean

“ (f, domain-object, codomain-object) ∈ Mor_{domain-object,codomain-object} ” .

Moreover, when domain-object and codomain-object are clear from the context, we sometimes write f instead of (f, domain − object, codomain − object).

Definition 1.2 (Functor)

Let C, D be categories.

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

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

with:

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

2. An arrow function F_{Arr}: _{C}Arr → _{D}Arr. We abbreviate “F_{Arr}(f)” by “_{f}F”.

3. ∀s, t ∈ _{C}Obj: ⟨_{C}Mor_{s,t}⟩F_{Obj} ⊆ _{D}Mor_{sF,tF}.

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

5. ∀f, g ∈ _{C}Arr: ( _{C}Cod(f) = _{C}Dom(g) ^{1} ⇒ _{(f _{C}⋄ g)}F = _{f}F _{D}⋄ _{g}F ).

Due to our special notation for the application of F_{Arr} 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”.

The identity functor 𝕀_{C} for C is the functor 𝕀_{C} := (_{_{C}Obj}|id,_{_{C}Arr}|id, C, C) . The composition of two functors F : B ↠ C and G : C ↠ D is the functor FG := (F_{Obj}∘G_{Obj}, F_{Arr}∘G_{Arr}, B, D) .

If (_{_{C}Obj}|id,_{_{C}Arr}|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.

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:

3. ∀s, t ∈_{C}Obj: ⟨_{C}Mor_{s,t}⟩F_{Obj} ⊆ _{D}Mor_{tF,sF}.

5. ∀f, g ∈ _{C}Arr: ( _{C}Cod(f) = _{C}Dom(g) ^{2} ⇒ _{fg}F = _{g}F_{f}F ).

1The condition “ _{C}Cod(f) = _{C}Dom(g) ” is necessary here because possibly

CCod(f) ≠ _{C}Dom(g) ∧ _{D}Cod(_{f}F) = _{D}Dom(_{g}F)

and then _{(f ⋄ g)}F is undefined while _{f}F ⋄_{g}F is defined.

2The condition “ _{C}Cod(f) = _{C}Dom(g) ” is necessary here because possibly

CCod(f) ≠ _{C}Dom(g) ∧ _{D}Cod(_{g}F) = _{D}Dom(_{f}F)

and then _{fg}F is undefined while _{g}F_{f}F is defined.

Definition 1.3 (Large Categories) A category C 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 1.4 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}Dom, CCod, C, and all functors F : C ↠ D are sets. If C is large, then _{C}⋄ , _{C}Arr, _{C}Dom, _{C}Cod, C, and all functors F : C ↠ D are proper classes.

2 Basic Examples

Example 2.1 (Categories of Sets) The relation category of sets is the large category REL given as follows:

RELObj := U RELMor_{A,B} := { (R, A, B) | R ⊆ A×B } for A, B ∈ U. (R, A, B) _{REL}⋄ (S, B, C) := (R∘S, A, C) for (R, A, B), (S, B, C) ∈ _{REL}Arr. RELId_{A} := (_{A}|id, A, A) for A ∈ U.

The partial function category of sets is the large sub-category FUN of the category REL given as follows:

FUNObj := U FUNMor_{A,B} := { (f, A, B) | f: A ⇝ B } for A, B ∈ U.

The (total function) category of sets is the large sub-category SET of the category FUN given as follows:

SETObj := U SETMor_{A,B} := { (f, A, B) | f: A → B } for A, B ∈ U.

Example 2.2 (Categories of Classes) The relation category of classes is the superlarge category RELCLASS given as follows:

RELCLASSObj is the collection of all classes A ⊆ U. RELCLASSMor_{A,B} is the collection all all classes R ⊆ A×B for A, B ⊆ U. (R, A, B) _{RELCLASS}⋄ (S, B, C) := (R∘S, A, C) for (R, A, B), (S, B, C) in _{RELCLASS}Arr. RELCLASSId_{A} := (_{A}|id, A, A) for A ⊆ U.

The (total function) category of classes is the superlarge sub-category CLASS of the superlarge category RELCLASS given as follows:

CLASSObj := _{RELCLASS}Obj CLASSMor_{A,B} is the collection of all (f, A, B) in _{RELCLASS}Mor_{A,B} with f: A → B.

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

SORTEDObj := 𝕊 → � (U) is the proper class of all 𝕊-sorted families of sets. RELCLASSMor_{A,B} := { f: 𝕊 → (U ⇝ U) | ∀s ∈ 𝕊: f_{s}: A_{s} → B_{s} } is the set of 𝕊-sorted

functions from A to B for A, B ∈ _{SORTED}Obj.

(f, A, B) _{SORTED}⋄ (g, B, C) := ((f_{s}∘g_{s})_{s∈𝕊}, A, C) for (f, A, B), (g, B, C) in _{SORTED}Arr. RELCLASSId_{A} := ((_{A_{s}}|id)_{s∈𝕊}, A, A) for A ∈ _{SORTED}Obj.

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^{3} category of C is the category Dual(C) given by Dual(C)Obj := _{C}Obj ; _{Dual(C)}Arr := _{C}Arr ; _{Dual(C)}Id_{s} := _{C}Id_{s} ; Dual(C)Dom := _{C}Cod ; _{Dual(C)}Cod := _{C}Dom ; f _{Dual(C)}⋄ g := g _{C}⋄ f ; _{Dual(C)}Mor_{s,t} := _{C}Mor_{t,s} .

Let F : C ↠ D. The dual functor Dual(F) : Dual(C) ↠ Dual(D) of F is given by Dual(F)_{Obj} := F_{Obj} ; Dual(F)_{Arr} := F_{Arr} . Do not confuse this co-variant functor with the contra-variant one having the same object and arrow functions: The dual contrafunctor Contradual(F) : C ⇌ Dual(D) of F is also given by Contradual(F)_{Obj} := F_{Obj}; Contradual(F)_{Arr} := F_{Arr}. Of special interest is Contradual(𝕀_{C}) : C ⇌ Dual(C), which is no co-variant functor: Note that C is in general not isomorphic to Dual(C).

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}, _{C}Dom with _{C}Cod, and _{C}Cod with _{C}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. Therefore, the dual of all categories and functors are all categories and functors. Moreover, 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, the dual of a consequence of a set of axioms A which is logically equivalent to its dual is a consequence 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.

3called 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

Now (w.r.t. C) f ∈ Arr is called …

… monic if ∀g, h ∈ Arr: ( gf = hf ⇒ g = h ).

… epi if ∀g, h ∈ Arr: ( fg = fh ⇒ g = h ).

Thus, “epi” is the dual of “monic”.

… split-monic if ∃r ∈ Arr: fr = Id_{Dom(f)}. Such an r is called a retraction of f.

… split-epi if ∃l ∈ Arr: lf = Id_{Cod(f)}. Such an l is called a section of f.

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

… an equalizer for p, q if fp = fq and ∀r ∈ Obj: ∀f′ ∈ Arr: ( f′p = f′q ⇒ ∃!h ∈ Arr: f′ = hf ).

… a co-equalizer for p, q if pf = qf and ∀u ∈ Obj: ∀f′ ∈ Arr: ( pf′ = qf′ ⇒ ∃!h ∈ Arr: f′ = fh ).

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

Lemma 4.2

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

Proof of Lemma 4.2 \underline{(1):} For gf = hf we get g = g Id_{Dom(f)} = gfr = hfr = h Id_{Dom(f)} = h. \underline{(2):} By the first property of an equalizer we get (gf)p = (gf)q for each g ∈ Arr with Cod(g) = Dom(f). Thus, (by the uniqueness part of the second property of an equalizer) gf = hf implies g = h.

Lemma 4.3 In the relation category^{4} 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.3 \underline{(1) ⇒ (2):} By Lemma 4.2. \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, A, B)(_{C}|id∘R^{−1}, B, A) = (_{A}|id, A, A) =_{REL}Id_{A}.

Lemma 4.4 In the relation category^{4} 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 (R,A,B)F := (R^{−1}, B, A) and since Lemma 4.4 is the F-isomorphic of the dual of Lemma 4.3, we do not give a proof of Lemma 4.4 — even if the duality principle^{5} is actually only sufficient to infer the logical equivalence of (1) and (2).

4Cf. Ex. 2.1.

5Cf. section 3.

Lemma 4.5 In the (total function) category^{6} 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.5 \underline{(1) ⇒ (2):} By Lemma 4.2. \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, gf = hf and g ≠ h, which contradicts (2). \underline{(3) ⇒ (1):} For p, q as indicated, we get fp = fq. 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.2. \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,∅} = ∅ .

6Cf. Ex. 2.1.

Lemma 4.6 In the (total function) category^{6} 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.6 \underline{(1) ⇒ (2):} By Lemma 4.2. \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 pf = qf. Furthermore, for f′::A→D with pf′ = qf′ 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′ = fh′, 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.2. \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 → � (U) 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 → U 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.7 In the partial function category^{7} 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.7 \underline{(1) ⇒ (2):} By Lemma 4.2. \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.5, we conclude that f is injective. \underline{(3) ⇒ (1):} For injective f: A ⇝ B we get f^{−1}::B→A and (f, A, B)(f^{−1}, B, A) = (_{dom(f)}|id, A, A) = (_{A}|id, A, A) = _{FUN}Id_{A}.

Lemma 4.8 In the partial function category^{7} 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.8 \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, fg = fh and g ≠ h, which contradicts the assumption that f::A→B is epi. \underline{(2) ⇒ (1):} Assume g, h::B→C with fg = fh. 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.2. \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.6.

7Cf. Ex. 2.1.

5 Algebras

A signature

sig = (𝔽, 𝕊, α)

consists of a set of function symbols 𝔽, a set of sorts 𝕊 (disjoint from 𝔽), and an arityfunction α: 𝔽 → 𝕊^{+}. For f ∈ 𝔽 its arity α(f) is the list of argument sorts augmented by the sort of the result of f.

A (total) sig/cons-algebra A over the signature sig = (𝔽, 𝕊, α) is classically defined to be a function defined on 𝔽 ⊎ 𝕊 with ∀s ∈ 𝕊: ∅ ≠ A_{s} and

f^{A}: A_{s_{0}...s_{n−1}} → A_{s_{n}} for f ∈ 𝔽 and α(f) = s_{0} … s_{n−1}s_{n}.

We write f^{A} instead of A(f) for f ∈ 𝔽 and A_{s_{0}...s_{n−1}} for A_{s_{0}}× ⋯ ×A_{s_{n−1}}.F ors ∈ 𝕊wecallA_{SIG,s}the universeof A forthesorts.

While this definition is very nice, it is not very well suited for category theory. The first step for comming to the categorical definition of an algebra is to encode α into a functor (F_{Obj}, F_{Arr}, SORTED, SORTED) from the category SORTED of 𝕊-sorted sets into itself.