- Functors
- Covariance and Contravariance
- Opposite Functors
- Hom Functors
- Bifunctors and multifunctors
- Endofunctor
- Forgetful Functor
- Free Functor
- Representable Functor

```
open import Agda.Primitive using (Level; _β_; lsuc; lzero)
open import Types.product
open import Types.relations
open import Types.equality
open import Category.category
open import Category.morphisms
module Category.functors where
```

Functors can be thought of as structure preserving maps or functions that operate on one category to produce another category, maintaining the categorical structure of the first category in the second category. Functors operate on both objects and morphisms of the first category.

Formally, let β and π» be two categories, then a functor π½ between them:

- Takes every object c β β to an object π½(c) β π»
- Takes every morphism \(f : c_1 β c_2\) β β to a morphism \(π½(f) : π½(c_1) β π½(c_2)\) in π» such that:
- \(π½(id_c) = id_{π½(c)}\)
- \(π½(g β f) = π½(g) β π½(f)\) for all \(f : c_1 β c_2\) and \(g : c_2 β c_3\) β β

Thus, functors preserve composition and identity morphisms of the source category in the target category.

Covariant functors are the vanilla functors we discussed in the previous section.

Contravariant functors are similar to covariant functors except that the functor reverses the direction of arrows in the target category.

Formally, let β and π» be two categories, then a contravariant functor π½ between them:

- Takes every object c β β to an object π½(c) β π»
- Takes every morphism \(f : c_1 β c_2\) β β to a morphism \(π½(f) : π½(c_2) β π½(c_1)\) in π» such that:
- \(π½(id_c) = id_{π½(c)}\)
- \(π½(g β f) = π½(f) β π½(g)\) for all \(f : c_1 β c_2\) and \(g : c_2 β c_3\) β β

Contravariant functors thus produce opposite categories. They can also be thought of as covariant functors from \(β^{op} β π»\) or as \(β β π»^{op}\) depending upon which one is convenient for working with. Contravariant functors play a very important role in various fields of mathematics, the most mentionable ones being presheaves and sheaves in algebraic topology are contravariant functors with some extra structure.

Every functor \(π½ : β β π»\) induces the opposite functor \(π½^{op} : β^{op} β π»^{op}\) such that \((π½^{op})^{op} = π½\).

For a category β, the set of all morphisms in β is called the Hom-set. If we take any object A β β, then the functor that maps any object X β β to the set of morphisms from A to X, i.e.Β Hom(A, X), is called the covariant Hom-functor. Similarly, the functor that maps any object X in β to the set of morphisms from X to A, i.e.Β Hom(X, A), is called a contravariant Hom-functor.

For a category β and a fixed object A β β, a covariant Hom-functor \(Hom(A, β) : A β Set\):

- Maps each object X β β to the set of morphisms of β, Hom(A, X)
- Maps each morphism \(f : X β Y\) to the morphism \(Hom(A, f) : Hom(A, X) β Hom(A, Y)\) where each h β Hom(A, f) takes some g β Hom(A, X) to \(f β g\)

For a category β and a fixed object A β β, a contravariant Hom-functor \(Hom(β, B) : B β Set\):

- Maps each object X β β to the set of morphisms of β, Hom(X, B)
- Maps each morphism \(f : X β Y\) to the morphism \(Hom(f, B) : Hom(X, B) β Hom(Y, B)\) where each h β Hom(f, A) takes some g β Hom(Y, B) to \(g β f\)

We define categories of the form πΈΓπΉ which is a cartesian product of two categories πΈ and πΉ as Cartesian categories. Given two functors \(π½ : πΈ β π\) and \(πΎ : πΉ β π\), we can define a functor on a product category πΈΓπΉ as the cartesian product of the individual functors π½ΓπΎ. Such a functor is called a bifunctor. We can extend this notion to multifunctors.

Endofunctors are functors that have the same source and target categories: \(π½ : β β β\).

Functors where the source category has more structure that the functor βforgetsβ while mapping it to the target category with lesser structure is called a forgetful functor. A functor from the category of Groups to the category of Sets which maps a group to its underlying set and a group homomorphism to its underlying function of sets is an example of a forgetful functor.

A free functor is the dual of the forgetful functor β instead of forgetting structure, it adds structure to its source category to get the target category. This addition of structure is done by using the source category as generators for generating free target categories. The free functor from Sets to Groups sends every set X to the free group generated by X and functions between sets to homomorphisms between free groups.

A representable functor sends a category to the category of sets. Representable functors represent an arbitrary category in the language of sets for studying the category in the more familiar language of sets.

Formally, a functor \(π½ : β β Set\) is a representable functor if it is naturally isomorphic to the hom-functor \(Hom_{β}(A, β)\), A β β.

- Sends every object \(X β β\) to the hom-set \(Hom_{β}(X, A)\)
- sends morphisms \(f : X' β X\) to \(F : (X β A) β (X' β X β A)\)

Dually, a contravariant functor \(πΎ : β^{op} β Set\) is representable if it is naturally isomorphic to the contravariant hom-functor \(Hom_{β}(β, A), A β β\).

- Sends every object \(X β β\) to the hom-set \(Hom_{β^{op}}(A, X)\)
- sends morphisms \(f : X β X'\) to \(F : (X β A) β (X' β X β A)\)

Though we have given a choppy definition of representable functors here without defining what βnatural isomorphismβ is, we will look deeper as they are one of the central concepts for building further structures of category theory.