Metamath Proof Explorer

Table of Contents - 8.1. Categories

1. Categories
   1. ccat
   2. ccid
   3. chomf
   4. ccomf
   5. df-cat
   6. df-cid
   7. df-homf
   8. df-comf
   9. iscat
   10. iscatd
   11. catidex
   12. catideu
   13. cidfval
   14. cidval
   15. cidffn
   16. cidfn
   17. catidd
   18. iscatd2
   19. catidcl
   20. catlid
   21. catrid
   22. catcocl
   23. catass
   24. catcone0
   25. 0catg
   26. 0cat
   27. homffval
   28. fnhomeqhomf
   29. homfval
   30. homffn
   31. homfeq
   32. homfeqd
   33. homfeqbas
   34. homfeqval
   35. comfffval
   36. comffval
   37. comfval
   38. comfffval2
   39. comffval2
   40. comfval2
   41. comfffn
   42. comffn
   43. comfeq
   44. comfeqd
   45. comfeqval
   46. catpropd
   47. cidpropd
2. Opposite category
   1. coppc
   2. df-oppc
   3. oppcval
   4. oppchomfval
   5. oppchomfvalOLD
   6. oppchom
   7. oppccofval
   8. oppcco
   9. oppcbas
   10. oppccatid
   11. oppchomf
   12. oppcid
   13. oppccat
   14. 2oppcbas
   15. 2oppchomf
   16. 2oppccomf
   17. oppchomfpropd
   18. oppccomfpropd
   19. oppccatf
3. Monomorphisms and epimorphisms
   1. cmon
   2. cepi
   3. df-mon
   4. df-epi
   5. monfval
   6. ismon
   7. ismon2
   8. monhom
   9. moni
   10. monpropd
   11. oppcmon
   12. oppcepi
   13. isepi
   14. isepi2
   15. epihom
   16. epii
4. Sections, inverses, isomorphisms
   1. csect
   2. cinv
   3. ciso
   4. df-sect
   5. df-inv
   6. df-iso
   7. sectffval
   8. sectfval
   9. sectss
   10. issect
   11. issect2
   12. sectcan
   13. sectco
   14. isofval
   15. invffval
   16. invfval
   17. isinv
   18. invss
   19. invsym
   20. invsym2
   21. invfun
   22. isoval
   23. inviso1
   24. inviso2
   25. invf
   26. invf1o
   27. invinv
   28. invco
   29. dfiso2
   30. dfiso3
   31. inveq
   32. isofn
   33. isohom
   34. isoco
   35. oppcsect
   36. oppcsect2
   37. oppcinv
   38. oppciso
   39. sectmon
   40. monsect
   41. sectepi
   42. episect
   43. sectid
   44. invid
   45. idiso
   46. idinv
   47. invisoinvl
   48. invisoinvr
   49. invcoisoid
   50. isocoinvid
   51. rcaninv
5. Isomorphic objects
   1. ccic
   2. df-cic
   3. cicfval
   4. brcic
   5. cic
   6. brcici
   7. cicref
   8. ciclcl
   9. cicrcl
   10. cicsym
   11. cictr
   12. cicer
6. Subcategories
   1. cssc
   2. cresc
   3. csubc
   4. df-ssc
   5. df-resc
   6. df-subc
   7. sscrel
   8. brssc
   9. sscpwex
   10. subcrcl
   11. sscfn1
   12. sscfn2
   13. ssclem
   14. isssc
   15. ssc1
   16. ssc2
   17. sscres
   18. sscid
   19. ssctr
   20. ssceq
   21. rescval
   22. rescval2
   23. rescbas
   24. reschom
   25. reschomf
   26. rescco
   27. resccoOLD
   28. rescabs
   29. rescabs2
   30. issubc
   31. issubc2
   32. 0ssc
   33. 0subcat
   34. catsubcat
   35. subcssc
   36. subcfn
   37. subcss1
   38. subcss2
   39. subcidcl
   40. subccocl
   41. subccatid
   42. subcid
   43. subccat
   44. issubc3
   45. fullsubc
   46. fullresc
   47. resscat
   48. subsubc
7. Functors
   1. cfunc
   2. cidfu
   3. ccofu
   4. cresf
   5. df-func
   6. df-idfu
   7. df-cofu
   8. df-resf
   9. relfunc
   10. funcrcl
   11. isfunc
   12. isfuncd
   13. funcf1
   14. funcixp
   15. funcf2
   16. funcfn2
   17. funcid
   18. funcco
   19. funcsect
   20. funcinv
   21. funciso
   22. funcoppc
   23. idfuval
   24. idfu2nd
   25. idfu2
   26. idfu1st
   27. idfu1
   28. idfucl
   29. cofuval
   30. cofu1st
   31. cofu1
   32. cofu2nd
   33. cofu2
   34. cofuval2
   35. cofucl
   36. cofuass
   37. cofulid
   38. cofurid
   39. resfval
   40. resfval2
   41. resf1st
   42. resf2nd
   43. funcres
   44. funcres2b
   45. funcres2
   46. wunfunc
   47. wunfuncOLD
   48. funcpropd
   49. funcres2c
8. Full & faithful functors
   1. cful
   2. cfth
   3. df-full
   4. df-fth
   5. fullfunc
   6. fthfunc
   7. relfull
   8. relfth
   9. isfull
   10. isfull2
   11. fullfo
   12. fulli
   13. isfth
   14. isfth2
   15. isffth2
   16. fthf1
   17. fthi
   18. ffthf1o
   19. fullpropd
   20. fthpropd
   21. fulloppc
   22. fthoppc
   23. ffthoppc
   24. fthsect
   25. fthinv
   26. fthmon
   27. fthepi
   28. ffthiso
   29. fthres2b
   30. fthres2c
   31. fthres2
   32. idffth
   33. cofull
   34. cofth
   35. coffth
   36. rescfth
   37. ressffth
   38. fullres2c
   39. ffthres2c
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
10. Initial, terminal and zero objects of a category
    1. cinito
    2. ctermo
    3. czeroo
    4. df-inito
    5. df-termo
    6. df-zeroo
    7. initofn
    8. termofn
    9. zeroofn
    10. initorcl
    11. termorcl
    12. zeroorcl
    13. initoval
    14. termoval
    15. zerooval
    16. isinito
    17. istermo
    18. iszeroo
    19. isinitoi
    20. istermoi
    21. initoid
    22. termoid
    23. dfinito2
    24. dftermo2
    25. dfinito3
    26. dftermo3
    27. initoo
    28. termoo
    29. iszeroi
    30. 2initoinv
    31. initoeu1
    32. initoeu1w
    33. initoeu2lem0
    34. initoeu2lem1
    35. initoeu2lem2
    36. initoeu2
    37. 2termoinv
    38. termoeu1
    39. termoeu1w