This page is under construction. - Ali
For precategories , there is a precategory , called the functor precategory, defined by
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 .
We define a natural isomorphism to be an isomorphism? in .
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
If is a precategory and is a category, then is a category.
Proof. 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 .
This reference needs to be included. For now as transports are not yet written up I didn’t bother including a reference to the page category. -Ali
But by [INCLUDE ME], 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.
Category theory functor category Rezk completion
Revision on September 6, 2018 at 10:55:38 by Ali Caglayan. See the history of this page for a list of all contributions to it.