Metamath Proof Explorer

Table of Contents - 8.4. Categorical constructions

1. Product of categories
   1. cxpc
   2. c1stf
   3. c2ndf
   4. cprf
   5. df-xpc
   6. df-1stf
   7. df-2ndf
   8. df-prf
   9. fnxpc
   10. xpcval
   11. xpcbas
   12. xpchomfval
   13. xpchom
   14. relxpchom
   15. xpccofval
   16. xpcco
   17. xpcco1st
   18. xpcco2nd
   19. xpchom2
   20. xpcco2
   21. xpccatid
   22. xpcid
   23. xpccat
   24. 1stfval
   25. 1stf1
   26. 1stf2
   27. 2ndfval
   28. 2ndf1
   29. 2ndf2
   30. 1stfcl
   31. 2ndfcl
   32. prfval
   33. prf1
   34. prf2fval
   35. prf2
   36. prfcl
   37. prf1st
   38. prf2nd
   39. 1st2ndprf
   40. catcxpccl
   41. xpcpropd
2. Functor evaluation
   1. cevlf
   2. ccurf
   3. cuncf
   4. cdiag
   5. df-evlf
   6. df-curf
   7. df-uncf
   8. df-diag
   9. evlfval
   10. evlf2
   11. evlf2val
   12. evlf1
   13. evlfcllem
   14. evlfcl
   15. curfval
   16. curf1fval
   17. curf1
   18. curf11
   19. curf12
   20. curf1cl
   21. curf2
   22. curf2val
   23. curf2cl
   24. curfcl
   25. curfpropd
   26. uncfval
   27. uncfcl
   28. uncf1
   29. uncf2
   30. curfuncf
   31. uncfcurf
   32. diagval
   33. diagcl
   34. diag1cl
   35. diag11
   36. diag12
   37. diag2
   38. diag2cl
   39. curf2ndf
3. Hom functor
   1. chof
   2. cyon
   3. df-hof
   4. df-yon
   5. hofval
   6. hof1fval
   7. hof1
   8. hof2fval
   9. hof2val
   10. hof2
   11. hofcllem
   12. hofcl
   13. oppchofcl
   14. yonval
   15. yoncl
   16. yon1cl
   17. yon11
   18. yon12
   19. yon2
   20. hofpropd
   21. yonpropd
   22. oppcyon
   23. oyoncl
   24. oyon1cl
   25. yonedalem1
   26. yonedalem21
   27. yonedalem3a
   28. yonedalem4a
   29. yonedalem4b
   30. yonedalem4c
   31. yonedalem22
   32. yonedalem3b
   33. yonedalem3
   34. yonedainv
   35. yonffthlem
   36. yoneda
   37. yonffth
   38. yoniso