Contents Previous Next


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:

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

Figure 1: Covariant Functor

Covariance and Contravariance

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:

Figure 2: Contravariant Functor

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.

Opposite Functors

Every functor \(𝔽 : β„‚ β†’ 𝔻\) induces the opposite functor \(𝔽^{op} : β„‚^{op} β†’ 𝔻^{op}\) such that \((𝔽^{op})^{op} = 𝔽\).

Hom Functors

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.

Covariant Hom-Functor

For a category β„‚ and a fixed object A ∈ β„‚, a covariant Hom-functor \(Hom(A, βˆ’) : A β†’ Set\):

Figure 3: Covariant hom functor

Contravariant Hom-Functor

For a category β„‚ and a fixed object A ∈ β„‚, a contravariant Hom-functor \(Hom(βˆ’, B) : B β†’ Set\):

Figure 4: Contravariant hom functor

Bifunctors and multifunctors

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: \(𝔽 : β„‚ β†’ β„‚\).

Forgetful Functor

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.

Free 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.

Representable Functor

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 ∈ β„‚.

Dually, a contravariant functor \(𝔾 : β„‚^{op} β†’ Set\) is representable if it is naturally isomorphic to the contravariant hom-functor \(Hom_{β„‚}(βˆ’, A), A ∈ β„‚\).

Figure 5: Representable Functor (contravariant)

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.

Natural Transformations