9.2 Functors and transformations
The following definitions are fairly obvious, and need no modification.
Since each type 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 and , the type of natural transformations from to is again a set.
Similarly, identity of functors is determined by identity of the functions and (transported along this) of the corresponding functions on hom-sets.
For precategories , there is a precategory defined by
is the type of functors from to .
is the type of natural transformations from to .
We define . Naturality follows by the unit axioms of a precategory. For and , we define . Naturality follows by associativity. Similarly, the unit and associativity laws for follow from those for . ∎
A natural transformation is an isomorphism in if and only if each is an isomorphism in .
If is an isomorphism, then we have that is its inverse. By definition of composition in , and similarly. Thus, and imply and , so is an isomorphism.
Conversely, suppose each is an isomorphism, with inverse called , say. We define a natural transformation with components ; for the naturality axiom we have
Now since composition and identity of natural transformations is determined on their components, we have and . ∎
The following result is fundamental.
If is a precategory and is a category, then is a category.
Let ; we must show that is an equivalence.
To give an inverse to it, suppose is a natural isomorphism. Then for any , we have an isomorphism , hence an identity . By function extensionality, we have an identity .
Now since the last two axioms of a functor are mere propositions, to show that it will suffice to show that for any , the functions
become equal when transported along . By computation for function extensionality, when applied to , becomes equal to . But by \autorefct:idtoiso-trans, transporting along and is equal to the composite , which by naturality of is equal to .
This completes the definition of a function . Now consider the composite
Since hom-sets are sets, their identity types are mere propositions, so to show that two identities are equal, it suffices to show that . But in the definition of , if were of the form , then would be equal to (this can easily be proved by induction on ). Thus, would be equal to , and so by function extensionality we would have , 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 we have . But as observed above, we have , while by computation for function extensionality. Since and are inverses, we have 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.
For functors and , their composite is given by
For each , the composite
It is easy to check the axioms.
For functors and and a natural transformation , the composite is given by
For each , the component .
Naturality is easy to check. Similarly, for as above and , the composite is given by
For each , the component .
For functors and and natural transformations and , we have
It suffices to check componentwise: at we have
|(by naturality of $\delta$)|
Classically, one defines the “horizontal composite” of and to be the common value of and . We will refrain from doing this, because while equal, these two transformations 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).
Composition of functors is associative: .
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.
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 or for either or , transporting along \autorefct:functor-assoc whenever necessary. We have a similar coherence result for units.
For a functor , we have equalities and , such that given also , the following triangle of equalities commutes.
See \autorefct:pre2cat,\autorefct:2cat for further development of these ideas.
|Title||9.2 Functors and transformations|