is the type of natural transformations from to . Proof. 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 .
Properties
Lemma 9.2.4
A natural transformation is an isomorphism in if and only if each is an isomorphism in .
Proof. If is an isomorphism?, then we have that is its inverse. By definition of composition in , . Thus, and imply that and , so is an isomorphism.
Conversely, suppose each is an isomorphism?, with inverse called . 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