Showing changes from revision #3 to #4:
Added | Removed | Changed
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 .
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.equivalence.
To give an inverse to it, suppose is a natural isomorphism. Then for anynatural isomorphism , . we Then have for an any isomorphism , hence we have an identityisomorphism? . By function extensionality, we have an identity, hence an identity . By function extensionality, we have an identity .
Now since the last two axioms of a functor are mere propositions, to show thatfunctor it are will suffice to show that for anymere propositions?, to show that it will suffice to show that for any , the functions
F_{a,b} hom_A(a,b) \to hom_B(Fa,Fb)\mathrlap{\qquad\text{and}}\\
G_{a,b}&:hom_A(a,b) \to hom_B(Ga,Gb)
become equal when transported along . By computation for function extensionality, when applied to , becomes equal to . But by \cref{ct:idtoiso-trans}, transporting along and is equal to the composite , which by naturality of is equal to .
become equal when transported along . By computation for function extensionality, when applied to , becomes equal to . But by \cref{ct: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
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.
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 eachnatural transformations we can have be tested componentwise, it suffices to show that for each . But as observed above, we have , . while But as observed above, we have , by while computation for function extensionality. Since and by computation for function extensionality. Since are and inverses, we have are inverses, we have as desired.
Category theory functor category Rezk completion
Revision on September 5, 2018 at 17:23:49 by Ali Caglayan. See the history of this page for a list of all contributions to it.