Functors and natural transformations

Functors and

natural transformations

functors ; category morphisms natural transformations ; functor morphisms

Functors and

natural transformations

functors ; category morphisms natural transformations ; functor morphisms

Functors

A functor F : K → K⁰ from a category K to a category K⁰ consists of:

• a function F : |K| → |K⁰|, and

• for all A, B ∈ |K|, a function F : K(A, B) → K⁰(F(A), F(B))

such that: Make explicit categories in which we work at various places here

• F preserves identities, i.e.,

F(id_A) = id_F(A) for all A ∈ |K|, and

• F preserves composition, i.e.,

F(f ;g) = F(f );F(g) for all f : A → B and g : B → C in K.

We really should differentiate between various components of F

Functors

A functor F : K → K⁰ from a category K to a category K⁰ consists of:

• a function F : |K| → |K⁰|, and

• for all A, B ∈ |K|, a function F : K(A, B) → K⁰(F(A), F(B))

such that: Make explicit categories in which we work at various places here

• F preserves identities, i.e.,

F(id_A) = id_F(A) for all A ∈ |K|, and

• F preserves composition, i.e.,

F(f ;g) = F(f );F(g)

Functors

A functor F : K → K⁰ from a category K to a category K⁰ consists of:

• a function F : |K| → |K⁰|, and

• for all A, B ∈ |K|, a function F : K(A, B) → K⁰(F(A), F(B))

such that: Make explicit categories in which we work at various places here

• F preserves identities, i.e.,

F(id_A) = id_F(A) for all A ∈ |K|, and

• F preserves composition, i.e.,

F(f ;g) = F(f );F(g) for all f : A → B and g : B → C in K.

We really should differentiate between various components of F

Functors

A functor F : K → K⁰ from a category K to a category K⁰ consists of:

• a function F : |K| → |K⁰|, and

• for all A, B ∈ |K|, a function F : K(A, B) → K⁰(F(A), F(B))

such that: Make explicit categories in which we work at various places here

• F preserves identities, i.e.,

F(id_A) = id_F(A) for all A ∈ |K|, and

• F preserves composition, i.e.,

F(f ;g) = F(f );F(g)

Functors

A functor F : K → K⁰ from a category K to a category K⁰ consists of:

• a function F : |K| → |K⁰|, and

• for all A, B ∈ |K|, a function F : K(A, B) → K⁰(F(A), F(B))

such that: Make explicit categories in which we work at various places here

• F preserves identities, i.e.,

F(id_A) = id_F(A) for all A ∈ |K|, and

• F preserves composition, i.e.,

F(f ;g) = F(f );F(g) for all f : A → B and g : B → C in K.

We really should differentiate between various components of F

Functors

A functor F : K → K⁰ from a category K to a category K⁰ consists of:

• a function F : |K| → |K⁰|, and

• for all A, B ∈ |K|, a function F : K(A, B) → K⁰(F(A), F(B))

such that: Make explicit categories in which we work at various places here

• F preserves identities, i.e.,

F(id_A) = id_F(A) for all A ∈ |K|, and

• F preserves composition, i.e.,

F(f ;g) = F(f );F(g)

Functors

A functor F : K → K⁰ from a category K to a category K⁰ consists of:

• a function F : |K| → |K⁰|, and

• for all A, B ∈ |K|, a function F : K(A, B) → K⁰(F(A), F(B))

such that: Make explicit categories in which we work at various places here

• F preserves identities, i.e.,

F(id_A) = id_F(A) for all A ∈ |K|, and

• F preserves composition, i.e.,

F(f ;g) = F(f );F(g) for all f : A → B and g : B → C in K.

We really should differentiate between various components of F

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor : P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor : P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P₋₁(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor : P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor : P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P₋₁(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by Set P - Set

X - 2^X

X⁰ - 2^X0

? f

? f~ -

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by Set P - Set

X - 2^X

X⁰ - 2^X0

? f

? f~ -

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P₋₁(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by Set P - Set

X - 2^X

X⁰ - 2^X0

? f

? f~ -

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by Set P - Set

X - 2^X

X⁰ - 2^X0

? f

? f~ -

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P₋₁(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by Set P - Set

X - 2^X

X⁰ - 2^X0

? f

? f~ -

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor : P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor: P₋₁: Set^op → Set given by

Set^op - Set P−1

X - 2^X

X⁰ - 2^X0

? 6

f

?

~f

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set| -

− P₋₁(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor: P₋₁: Set^op → Set given by

Set^op - Set P−1

X - 2^X

6

f - ~f

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor: P₋₁: Set^op → Set given by

Set^op - Set P−1

X - 2^X

X⁰ - 2^X0

? 6

f

?

~f

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set| -

− P₋₁(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor: P₋₁: Set^op → Set given by

Set^op - Set P−1

X - 2^X

6

op Set f

~f

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set| -

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor: P₋₁: Set^op → Set given by

Set^op - Set P−1

X - 2^X

X⁰ - 2^X0

? 6 f

inSet

?

~f

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set| -

− P−1(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor: P₋₁: Set^op → Set given by

Set^op - Set P−1

X - 2^X

6

Set f - ~f

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

Examples

• identity functors: Id_K: K → K, for any category K

• inclusions: I_K,→K⁰ : K → K⁰, for any subcategory K of K⁰

• constant functors: C_A: K → K⁰, for any categories K, K⁰ and A ∈ |K⁰|, with C_A(f ) = id_A for all morphisms f in K

• powerset functor: P : Set → Set given by

− P(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P(f ) : P(X) → P(X⁰) for all f : X → X⁰ in Set, P(f )(Y ) = {f (y) | y ∈ Y } for all Y ⊆ X

• contravariant powerset functor: P₋₁: Set^op → Set given by

− P₋₁(X) = {Y | Y ⊆ X}, for all X ∈ |Set|

− P−1(f ) : P(X) → P(X⁰) for all f : X⁰ → X in Set, P₋₁(f )(Y ) = {x⁰ ∈ X⁰ | f (x⁰) ∈ Y } for all Y ⊆ X

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor : List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b , i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b , i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X Set List- Monoid

X - hX∗, b , i

X⁰ -h(X⁰)∗, b , i

? f

? f ∗ -

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X Set List- Monoid

X - hX∗, b, i

f - f ∗

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X Set List- Monoid

X - hX∗, b, i

X⁰ -h(X⁰)∗, b, i

? f

? f ∗ -

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X Set List- Monoid

X - hX∗, b, i

f - f ∗

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X Set List- Monoid

X - hX∗, b, i

X⁰ -h(X⁰)∗, b, i

? f

? f ∗ -

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X

• totalisation functor: Tot : Pfn → Set∗, where Set∗ is the subcategory of Set of sets with a distinguished element ∗ and ∗-preserving functions

− Tot(X) = X ] {∗} Define Set∗ as the category of algebras



 f (x) if it is defined

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X

• totalisation functor: Tot : Pfn → Set∗, where Set∗ is the subcategory of Set of sets with a distinguished element ∗ and ∗-preserving functions

− Tot(X) = X ] {∗} Define Set∗ as the category of algebras

− Tot(f )(x) =







f (x) if it is defined

∗ otherwise

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X

• totalisation functor: Tot : Pfn → Set∗, where Set∗ is the subcategory of Set of sets with a distinguished element ∗ and ∗-preserving functions

− Tot(X) = X ] {∗} Define Set∗ as the category of algebras



 f (x) if it is defined

Examples, cont’d.

• projection functors: π₁: K × K⁰ → K, π₂ : K × K⁰ → K⁰

• list functor: List : Set → Monoid, where Monoid is the category of monoids (as objects) with monoid homomorphisms as morphisms:

− List(X) = hX∗, b, i, for all X ∈ |Set|, where X∗ is the set of all finite lists of elements from X, b is the list concatenation, and  is the empty list.

− List(f ) : List(X) → List(X⁰) for f : X → X⁰ in Set,

List(f )(hx₁, . . . , x_ni) = hf (x₁), . . . , f (x_n)i for all x₁, . . . , x_n ∈ X

• totalisation functor: Tot : Pfn → Set∗, where Set∗ is the subcategory of Set of sets with a distinguished element ∗ and ∗-preserving functions

− Tot(X) = X ] {∗} Define Set∗ as the category of algebras

− Tot(f )(x) =







f (x) if it is defined

∗ otherwise

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all n ∈ N and D^A_e = id_A for all e ∈ E

− ∆^G_K(f ) = µ^f : D^A → D^B, for all f : A → B, where µ^f_n = f for all n ∈ N

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all n ∈ N and D^A_e = id_A for all e ∈ E

− ∆^G_K(f ) = µ^f : D^A → D^B, for all f : A → B, where µ^f_n = f for all n ∈ N

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all n ∈ N and D^A_e = id_A for all e ∈ E

− ∆^G_K(f ) = µ^f : D^A → D^B, for all f : A → B, where µ^f_n = f for all n ∈ N

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all n ∈ N and D^A_e = id_A for all e ∈ E

− ∆^G_K(f ) = µ^f : D^A → D^B, for all f : A → B, where µ^f_n = f for all n ∈ N

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all

Examples, cont’d.

• carrier set functors: | | : Alg(Σ) → Set^S, for any algebraic signature Σ = hS, Ωi, yielding the algebra carriers and homomorphisms as functions between them

• reduct functors: _σ : Alg(Σ⁰) → Alg(Σ), for any signature morphism σ : Σ → Σ⁰, as defined earlier

• term algebra functors: T_Σ: Set → Alg(Σ) for all (single-sorted) algebraic

signatures Σ ∈ |AlgSig| Generalise to many-sorted signatures

− T_Σ(X) = T_Σ(X) for all X ∈ |Set|

− T_Σ(f ) = f^#: T_Σ(X) → T_Σ(X⁰) for all functions f : X → X⁰

• diagonal functors: ∆^G_K: K → Diag^G_K for any graph G with nodes N = |G|_nodes and edges E = |G|_edges, and category K

− ∆^G_K(A) = D^A, where D^A is the “constant” diagram, with D_n^A = A for all n ∈ N and D^A_e = id_A for all e ∈ E

− ∆^G_K(f ) = µ^f : D^A → D^B, for all f : A → B, where µ^f_n = f for all n ∈ N

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor , contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

A

B

 

K(A, B)

?

A⁰

B⁰

 

K(A⁰, B⁰)

?

 f

- g

h

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor, contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

Also: Hom_K(A, ) : K → Set Hom_K( , B) : K^op → Set

A

B





K(A, B)

?

A⁰

B⁰





K(A⁰, B⁰)

?

 f

- g

Hom_K(f, g) 6 h

h - f ;h;g

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor, contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

A

B

 

K(A, B)

?

A⁰

B⁰

 

K(A⁰, B⁰)

?

 f

- g

h

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor, contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

Also: Hom_K(A, ) : K → Set Hom_K( , B) : K^op → Set

A

B





K(A, B)

?

A⁰

B⁰





K(A⁰, B⁰)

?

 f

- g

Hom_K(f, g) 6 h

h - f ;h;g

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor, contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

A

B

 

K(A, B)

?

A⁰

B⁰

 

K(A⁰, B⁰)

?

 f

- g

h

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor, contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

Also: Hom_K(A, ) : K → Set Hom_K( , B) : K^op → Set

A

B





K(A, B)

?

A⁰

B⁰





K(A⁰, B⁰)

?

 f

- g

Hom_K(f, g) 6 h

h - f ;h;g

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor, contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

A

B

 

K(A, B)

?

A⁰

B⁰

 

K(A⁰, B⁰)

?

 f

- g

h

Hom-functors

Given a locally small category K, define

Hom_K: K^op × K → Set

a binary hom-functor, contravariant on the first argument and covariant on the second argument, as follows:

• Hom_K(hA, Bi) = K(A, B), for all hA, Bi ∈ |K^op × K|, i.e., A, B ∈ |K|

• Hom_K(hf, gi) : K(A, B) → K(A⁰, B⁰), for hf, gi : hA, Bi → hA⁰, B⁰i in K^op × K, i.e., f : A⁰ → A and g : B → B⁰ in K, as a function given by Hom_K(hf, gi)(h) = f ;h;g.

Also: Hom_K(A, ) : K → Set Hom_K( , B) : K^op → Set

A

B





K(A, B)

?

A⁰

B⁰





K(A⁰, B⁰)

?

 f

- g

Hom_K(f, g) 6 h

h - f ;h;g

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰ If f : A → B is mono in K then

F(f ) : F(A) → F(B) is mono in K⁰ ??

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰ If f : A → B is epi in K then

F(f ) : F(A) → F(B) is epi in K⁰ ??

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

If f : A → B is a retraction in K then

F(f ) : F(A) → F(B) is a retraction in K⁰ ??

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰ If f : A → B is iso in K then

F(f ) : F(A) → F(B) is iso in K⁰ ??

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

If α : X → D is a cone on diagram D in K then F(α) : F(X) → F(D) is a cone on dia- gram F(D) in K⁰ ??

BTW:

• F(D) has the same shape as D, i.e. G(F(D)) = G(D)

(with nodes N and edges E)

− (F(D))_n = F(D_n) for n ∈ N

− (F(D))_e = F(D_e) for e ∈ E

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

If α : X → D is a limit of diagram D in K then F(α) : F(X) → F(D) is a limit of diagram F(D) in K⁰ ??

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰ . . .

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

• A functor is (finitely) continuous if it preserves all existing (finite) limits.

Which of the above functors are (finitely) continuous?

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

• A functor is (finitely) continuous if it preserves all existing (finite) limits.

Which of the above functors are (finitely) continuous?

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

• A functor is (finitely) continuous if it preserves all existing (finite) limits.

Which of the above functors are (finitely) continuous?

Functors preserve. . .

• Check whether functors preserve:

− monomorphisms

− epimorphisms

− (co)retractions

− isomorphisms

− (co)cones

− (co)limits

− . . .

F : K → K⁰

• A functor is (finitely) continuous if it preserves all existing (finite) limits.

Which of the above functors are (finitely) continuous?

Functors compose. . .

Given two functors F : K → K⁰ and G : K⁰ → K⁰⁰, their composition F;G : K → K⁰⁰ is defined as expected:

• (F;G)(A) = G(F(A)) for all A ∈ |K|

• (F;G)(f ) = G(F(f )) for all f : A → B in K

Cat, the category of (sm)all categories

− objects: (sm)all categories

− morphisms: functors between them

− composition: as above

Characterise isomorphisms in Cat Define products, terminal objects, equalisers and pullback in Cat

Try to define their duals

Functors compose. . .

Given two functors F : K → K⁰ and G : K⁰ → K⁰⁰, their composition F;G : K → K⁰⁰ is defined as expected:

• (F;G)(A) = G(F(A)) for all A ∈ |K|

• (F;G)(f ) = G(F(f )) for all f : A → B in K

Cat, the category of (sm)all categories

− objects: (sm)all categories

− morphisms: functors between them

− composition: as above

Characterise isomorphisms in Cat Define products, terminal objects, equalisers and pullback in Cat

Functors compose. . .

Given two functors F : K → K⁰ and G : K⁰ → K⁰⁰, their composition F;G : K → K⁰⁰ is defined as expected:

• (F;G)(A) = G(F(A)) for all A ∈ |K|

• (F;G)(f ) = G(F(f )) for all f : A → B in K

Cat, the category of (sm)all categories

− objects: (sm)all categories

− morphisms: functors between them

− composition: as above

Characterise isomorphisms in Cat Define products, terminal objects, equalisers and pullback in Cat

Try to define their duals

Functors compose. . .

Given two functors F : K → K⁰ and G : K⁰ → K⁰⁰, their composition F;G : K → K⁰⁰ is defined as expected:

• (F;G)(A) = G(F(A)) for all A ∈ |K|

• (F;G)(f ) = G(F(f )) for all f : A → B in K

Cat, the category of (sm)all categories

− objects: (sm)all categories

− morphisms: functors between them

− composition: as above

Characterise isomorphisms in Cat Define products, terminal objects, equalisers and pullback in Cat