Metamath Proof Explorer

Table of Contents - 8.1.9. Natural transformations and the functor category

1. cnat
2. cfuc
3. df-nat
4. df-fuc
5. fnfuc
6. natfval
7. isnat
8. isnat2
9. natffn
10. natrcl
11. nat1st2nd
12. natixp
13. natcl
14. natfn
15. nati
16. wunnat
17. wunnatOLD
18. catstr
19. fucval
20. fuccofval
21. fucbas
22. fuchom
23. fuchomOLD
24. fucco
25. fuccoval
26. fuccocl
27. fucidcl
28. fuclid
29. fucrid
30. fucass
31. fuccatid
32. fuccat
33. fucid
34. fucsect
35. fucinv
36. invfuc
37. fuciso
38. natpropd
39. fucpropd