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. 0catg
   25. 0cat
   26. homffval
   27. fnhomeqhomf
   28. homfval
   29. homffn
   30. homfeq
   31. homfeqd
   32. homfeqbas
   33. homfeqval
   34. comfffval
   35. comffval
   36. comfval
   37. comfffval2
   38. comffval2
   39. comfval2
   40. comfffn
   41. comffn
   42. comfeq
   43. comfeqd
   44. comfeqval
   45. catpropd
   46. cidpropd
2. Opposite category
   1. coppc
   2. df-oppc
   3. oppcval
   4. oppchomfval
   5. oppchom
   6. oppccofval
   7. oppcco
   8. oppcbas
   9. oppccatid
   10. oppchomf
   11. oppcid
   12. oppccat
   13. 2oppcbas
   14. 2oppchomf
   15. 2oppccomf
   16. oppchomfpropd
   17. oppccomfpropd
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. rescabs
   28. rescabs2
   29. issubc
   30. issubc2
   31. 0ssc
   32. 0subcat
   33. catsubcat
   34. subcssc
   35. subcfn
   36. subcss1
   37. subcss2
   38. subcidcl
   39. subccocl
   40. subccatid
   41. subcid
   42. subccat
   43. issubc3
   44. fullsubc
   45. fullresc
   46. resscat
   47. 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. funcpropd
   48. 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. catstr
   18. fucval
   19. fuccofval
   20. fucbas
   21. fuchom
   22. fucco
   23. fuccoval
   24. fuccocl
   25. fucidcl
   26. fuclid
   27. fucrid
   28. fucass
   29. fuccatid
   30. fuccat
   31. fucid
   32. fucsect
   33. fucinv
   34. invfuc
   35. fuciso
   36. natpropd
   37. 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. initorcl
    8. termorcl
    9. zeroorcl
    10. initoval
    11. termoval
    12. zerooval
    13. isinito
    14. istermo
    15. iszeroo
    16. isinitoi
    17. istermoi
    18. initoid
    19. termoid
    20. initoo
    21. termoo
    22. iszeroi
    23. 2initoinv
    24. initoeu1
    25. initoeu1w
    26. initoeu2lem0
    27. initoeu2lem1
    28. initoeu2lem2
    29. initoeu2
    30. 2termoinv
    31. termoeu1
    32. termoeu1w