9.2 Functors and transformations

The following definitions are fairly obvious, and need no modification.

Definition 9.2.1.

Let A and B be precategories. A functorMathworldPlanetmath F:AB consists of

  1. 1.

    A function F0:A0B0, generally also denoted F.

  2. 2.

    For each a,b:A, a function Fa,b:homA(a,b)homB(Fa,Fb), generally also denoted F.

  3. 3.

    For each a:A, we have F(1a)=1Fa.

  4. 4.

    For each a,b,c:A and f:homA(a,b) and g:homB(b,c), we have


Note that by inductionMathworldPlanetmath on identityPlanetmathPlanetmathPlanetmathPlanetmath, a functor also preserves 𝗂𝖽𝗍𝗈𝗂𝗌𝗈.

Definition 9.2.2.

For functors F,G:AB, a natural transformation γ:FG consists of

  1. 1.

    For each a:A, a morphismMathworldPlanetmath γa:homB(Fa,Ga) (the “components”).

  2. 2.

    For each a,b:A and f:homA(a,b), we have Gfγa=γbFf (the “naturality axiom”).

Since each type homB(Fa,Gb) is a set, its identity type is a mere proposition. Thus, the naturality axiom is a mere proposition, so identity of natural transformations is determined by identity of their components. In particular, for any F and G, the type of natural transformations from F to G is again a set.

Similarly, identity of functors is determined by identity of the functions A0B0 and (transported along this) of the corresponding functions on hom-sets.

Definition 9.2.3.

For precategories A,B, there is a precategory BA defined by

  • (BA)0 is the type of functors from A to B.

  • homBA(F,G) is the type of natural transformations from F to G.


We define (1F)a:1Fa. Naturality follows by the unit axioms of a precategory. For γ:FG and δ:GH, we define (δγ)a:δaγa. Naturality follows by associativity. Similarly, the unit and associativity laws for BA follow from those for B. ∎

Lemma 9.2.4.

A natural transformation γ:FG is an isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath in BA if and only if each γa is an isomorphism in B.


If γ is an isomorphism, then we have δ:GF that is its inverseMathworldPlanetmathPlanetmathPlanetmath. By definition of composition in BA, (δγ)aδaγa and similarly. Thus, δγ=1F and γδ=1G imply δaγa=1Fa and γaδa=1Ga, so γa is an isomorphism.

Conversely, suppose each γa is an isomorphism, with inverse called δa, say. We define a natural transformation δ:GF with components δa; for the naturality axiom we have


Now since composition and identity of natural transformations is determined on their components, we have γδ=1G and δγ=1F. ∎

The following result is fundamental.

Theorem 9.2.5.

If A is a precategory and B is a category, then BA is a category.


Let F,G:AB; we must show that 𝗂𝖽𝗍𝗈𝗂𝗌𝗈:(F=G)(FG) is an equivalence.

To give an inverse to it, suppose γ:FG is a natural isomorphism. Then for any a:A, we have an isomorphism γa:FaGa, hence an identity 𝗂𝗌𝗈𝗍𝗈𝗂𝖽(γa):Fa=Ga. By function extensionality, we have an identity γ¯:F0=(A0B0)G0.

Now since the last two axioms of a functor are mere propositions, to show that F=G it will suffice to show that for any a,b:A, the functions

Fa,b :homA(a,b)homB(Fa,Fb)\mathrlap  and
Ga,b :homA(a,b)homB(Ga,Gb)

become equal when transported along γ¯. By computation for function extensionality, when applied to a, γ¯ becomes equal to 𝗂𝗌𝗈𝗍𝗈𝗂𝖽(γa). But by \autorefct:idtoiso-trans, transporting Ff:homB(Fa,Fb) along 𝗂𝗌𝗈𝗍𝗈𝗂𝖽(γa) and 𝗂𝗌𝗈𝗍𝗈𝗂𝖽(γb) is equal to the composite γbFf(γa)-1, which by naturality of γ is equal to Gf.

This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the definition of a function (FG)(F=G). Now consider the composite


Since hom-sets are sets, their identity types are mere propositions, so to show that two identities p,q:F=G are equal, it suffices to show that p=F0=G0q. But in the definition of γ¯, if γ were of the form 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(p), then γa would be equal to 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(pa) (this can easily be proved by induction on p). Thus, 𝗂𝗌𝗈𝗍𝗈𝗂𝖽(γa) would be equal to pa, and so by function extensionality we would have γ¯=p, which is what we need.

Finally, consider the composite


Since identity of natural transformations can be tested componentwise, it suffices to show that for each a we have 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(γ¯)a=γa. But as observed above, we have 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(γ¯)a=𝗂𝖽𝗍𝗈𝗂𝗌𝗈((γ¯)a), while (γ¯)a=𝗂𝗌𝗈𝗍𝗈𝗂𝖽(γa) by computation for function extensionality. Since 𝗂𝗌𝗈𝗍𝗈𝗂𝖽 and 𝗂𝖽𝗍𝗈𝗂𝗌𝗈 are inverses, we have 𝗂𝖽𝗍𝗈𝗂𝗌𝗈(γ¯)a=γa as desired. ∎

In particular, naturally isomorphic functors between categories (as opposed to precategories) are equal.

We now define all the usual ways to compose functors and natural transformations.

Definition 9.2.6.

For functors F:AB and G:BC, their composite GF:AC is given by

  • The composite (G0F0):A0C0

  • For each a,b:A, the composite


It is easy to check the axioms.

Definition 9.2.7.

For functors F:AB and G,H:BC and a natural transformation γ:GH, the composite (γF):GFHF is given by

  • For each a:A, the component γFa.

Naturality is easy to check. Similarly, for γ as above and K:CD, the composite (Kγ):KGKH is given by

  • For each b:B, the component K(γb).

Lemma 9.2.8.

For functors F,G:AB and H,K:BC and natural transformations γ:FG and δ:HK, we have


It suffices to check componentwise: at a:A we have

((δG)(Hγ))a (δG)a(Hγ)a
=K(γa)δFa (by naturality of $\delta$)

Classically, one defines the “horizontal composite” of γ:FG and δ:HK to be the common value of (δG)(Hγ) and (Kγ)(δF). We will refrain from doing this, because while equal, these two transformationsPlanetmathPlanetmath are not definitionally equal. This also has the consequence that we can use the symbol (or juxtaposition) for all kinds of composition unambiguously: there is only one way to compose two natural transformations (as opposed to composing a natural transformation with a functor on either side).

Lemma 9.2.9.

Composition of functors is associative: H(GF)=(HG)F.


Since composition of functions is associative, this follows immediately for the actions on objects and on homs. And since hom-sets are sets, the rest of the data is automatic. ∎

The equality in \autorefct:functor-assoc is likewise not definitional. (Composition of functions is definitionally associative, but the axioms that go into a functor must also be composed, and this breaks definitional associativity.) For this reason, we need also to know about coherence for associativity.

Lemma 9.2.10.

ct:functor-assoc is coherent, i.e. the following pentagon of equalities commutes:


As in \autorefct:functor-assoc, this is evident for the actions on objects, and the rest is automatic. ∎

We will henceforth abuse notation by writing HGF or HGF for either H(GF) or (HG)F, transporting along \autorefct:functor-assoc whenever necessary. We have a similar coherence result for units.

Lemma 9.2.11.

For a functor F:AB, we have equalities (1BF)=F and (F1A)=F, such that given also G:BC, the following triangle of equalities commutes.


See \autorefct:pre2cat,\autorefct:2cat for further development of these ideas.

Title 9.2 Functors and transformations