Metamath Proof Explorer

Table of Contents - 21.53.16. Examples of categories

1. The category of categories
   1. catcrcl
   2. catcrcl2
   3. elcatchom
   4. catcsect
   5. catcinv
   6. catcisoi
   7. uobeq2
   8. uobeq3
   9. opf11
   10. opf12
   11. opf2fval
   12. opf2
   13. fucoppclem
   14. fucoppcid
   15. fucoppcco
   16. fucoppc
   17. fucoppcffth
   18. fucoppcfunc
   19. fucoppccic
   20. oppfdiag1
   21. oppfdiag1a
   22. oppfdiag
2. Thin categories
   1. cthinc
   2. df-thinc
   3. isthinc
   4. isthinc2
   5. isthinc3
   6. thinccat
   7. thinccatd
   8. thincssc
   9. isthincd2lem1
   10. thincmo2
   11. thinchom
   12. thincmo
   13. thincmoALT
   14. thincmod
   15. thincn0eu
   16. thincid
   17. thincmon
   18. thincepi
   19. isthincd2lem2
   20. isthincd
   21. isthincd2
   22. oppcthin
   23. oppcthinco
   24. oppcthinendc
   25. oppcthinendcALT
   26. thincpropd
   27. subthinc
   28. functhinclem1
   29. functhinclem2
   30. functhinclem3
   31. functhinclem4
   32. functhinc
   33. functhincfun
   34. fullthinc
   35. fullthinc2
   36. thincfth
   37. thincciso
   38. thinccisod
   39. thincciso2
   40. thincciso3
   41. thincciso4
   42. 0thincg
   43. 0thinc
   44. indcthing
   45. discthing
   46. indthinc
   47. indthincALT
   48. prsthinc
   49. setcthin
   50. setc2othin
   51. thincsect
   52. thincsect2
   53. thincinv
   54. thinciso
   55. thinccic
3. Terminal categories
   1. ctermc
   2. df-termc
   3. istermc
   4. istermc2
   5. istermc3
   6. termcthin
   7. termcthind
   8. termccatd
   9. termcbas
   10. termco
   11. termcbas2
   12. termcbasmo
   13. termchomn0
   14. termchommo
   15. termcid
   16. termcid2
   17. termchom
   18. termchom2
   19. setcsnterm
   20. setc1oterm
   21. setc1obas
   22. setc1ohomfval
   23. setc1ocofval
   24. setc1oid
   25. funcsetc1ocl
   26. funcsetc1o
   27. isinito2lem
   28. isinito2
   29. isinito3
   30. dfinito4
   31. dftermo4
   32. termcpropd
   33. oppctermhom
   34. oppctermco
   35. oppcterm
   36. functermclem
   37. functermc
   38. functermc2
   39. functermceu
   40. fulltermc
   41. fulltermc2
   42. termcterm
   43. termcterm2
   44. termcterm3
   45. termcciso
   46. termccisoeu
   47. termc2
   48. termc
   49. dftermc2
   50. eufunclem
   51. eufunc
   52. idfudiag1lem
   53. idfudiag1bas
   54. idfudiag1
   55. euendfunc
   56. euendfunc2
   57. termcarweu
   58. arweuthinc
   59. arweutermc
   60. dftermc3
   61. termcfuncval
   62. diag1f1olem
   63. diag1f1o
   64. termcnatval
   65. diag2f1olem
   66. diag2f1o
   67. diagffth
   68. diagciso
   69. diagcic
   70. funcsn
   71. fucterm
   72. 0fucterm
   73. termfucterm
   74. cofuterm
   75. uobeqterm
   76. isinito4
   77. isinito4a
4. Preordered sets as thin categories
   1. cprstc
   2. df-prstc
   3. prstcval
   4. prstcnidlem
   5. prstcnid
   6. prstcbas
   7. prstcleval
   8. prstcle
   9. prstcocval
   10. prstcoc
   11. prstchomval
   12. prstcprs
   13. prstcthin
   14. prstchom
   15. prstchom2
   16. prstchom2ALT
   17. oduoppcbas
   18. oduoppcciso
   19. postcpos
   20. postcposALT
   21. postc
   22. discsntermlem
   23. basrestermcfolem
   24. discbas
   25. discthin
   26. discsnterm
   27. basrestermcfo
   28. termcnex
5. Monoids as categories
   1. cmndtc
   2. df-mndtc
   3. mndtcval
   4. mndtcbasval
   5. mndtcbaseu
   6. mndtcob
   7. mndtcobeq
   8. mndtchom
   9. mndtcco
   10. mndtcco2
   11. mndtccatid
   12. mndtccat
   13. mndtcid
   14. oppgoppchom
   15. oppgoppcco
   16. oppgoppcid
   17. grptcmon
   18. grptcepi
6. Categories with at most one object and at most two morphisms
   1. 2arwcatlem1
   2. 2arwcatlem2
   3. 2arwcatlem3
   4. 2arwcatlem4
   5. 2arwcatlem5
   6. 2arwcat
   7. incat
   8. setc1onsubc
   9. cnelsubclem
   10. cnelsubc