Metamath Proof Explorer

Table of Contents - 21.51.15. Categories

1. Categories
   1. homf0
   2. catprslem
   3. catprs
   4. catprs2
   5. catprsc
   6. catprsc2
   7. endmndlem
2. Opposite category
   1. oppccatb
   2. oppcmndclem
   3. oppcendc
   4. oppcmndc
3. Monomorphisms and epimorphisms
   1. idmon
   2. idepi
4. Sections, inverses, isomorphisms
   1. sectrcl
   2. sectrcl2
   3. invrcl
   4. invrcl2
   5. isinv2
   6. isisod
   7. upeu2lem
   8. sectfn
   9. invfn
   10. isofnALT
   11. isofval2
   12. isorcl
   13. isorcl2
   14. isoval2
   15. sectpropdlem
   16. sectpropd
   17. invpropdlem
   18. invpropd
   19. isopropdlem
   20. isopropd
5. Isomorphic objects
   1. cicfn
   2. cicrcl2
   3. oppccic
   4. relcic
   5. cicerALT
   6. cic1st2nd
   7. cic1st2ndbr
   8. cicpropdlem
   9. cicpropd
   10. oppccicb
   11. oppcciceq
6. Subcategories
   1. dmdm
   2. iinfssclem1
   3. iinfssclem2
   4. iinfssclem3
   5. iinfssc
   6. iinfsubc
   7. iinfprg
   8. infsubc
   9. infsubc2
   10. infsubc2d
   11. discsubclem
   12. discsubc
   13. iinfconstbaslem
   14. iinfconstbas
   15. nelsubclem
   16. nelsubc
   17. nelsubc2
   18. nelsubc3lem
   19. nelsubc3
   20. ssccatid
   21. resccatlem
   22. resccat
7. Functors
   1. reldmfunc
   2. func1st2nd
   3. func1st
   4. func2nd
   5. funcrcl2
   6. funcrcl3
   7. funcf2lem
   8. funcf2lem2
   9. 0funcglem
   10. 0funcg2
   11. 0funcg
   12. 0funclem
   13. 0func
   14. 0funcALT
   15. func0g
   16. func0g2
   17. initc
   18. cofu1st2nd
   19. rescofuf
   20. cofu1a
   21. cofu2a
   22. cofucla
   23. funchomf
   24. idfurcl
   25. idfu1stf1o
   26. idfu1stalem
   27. idfu1sta
   28. idfu1a
   29. idfu2nda
   30. imasubclem1
   31. imasubclem2
   32. imasubclem3
   33. imaf1homlem
   34. imaf1hom
   35. imaidfu2lem
   36. imaidfu
   37. imaidfu2
   38. cofid1a
   39. cofid2a
   40. cofid1
   41. cofid2
   42. cofidvala
   43. cofidf2a
   44. cofidf1a
   45. cofidval
   46. cofidf2
   47. cofidf1
8. Opposite functors
   1. coppf
   2. df-oppf
   3. oppffn
   4. reldmoppf
   5. oppfvalg
   6. oppfrcllem
   7. oppfrcl
   8. oppfrcl2
   9. oppfrcl3
   10. oppf1st2nd
   11. 2oppf
   12. eloppf
   13. eloppf2
   14. oppfvallem
   15. oppfval
   16. oppfval2
   17. oppfval3
   18. oppf1
   19. oppf2
   20. oppfoppc
   21. oppfoppc2
   22. funcoppc2
   23. funcoppc4
   24. funcoppc5
   25. 2oppffunc
   26. funcoppc3
   27. oppff1
   28. oppff1o
   29. cofuoppf
9. Full & faithful functors
   1. imasubc
   2. imasubc2
   3. imassc
   4. imaid
   5. imaf1co
   6. imasubc3
   7. fthcomf
   8. idfth
   9. idemb
   10. idsubc
   11. idfullsubc
   12. cofidfth
   13. fulloppf
   14. fthoppf
   15. ffthoppf
10. Universal property
    1. upciclem1
    2. upciclem2
    3. upciclem3
    4. upciclem4
    5. upcic
    6. upeu
    7. upeu2
    8. cup
    9. df-up
    10. reldmup
    11. upfval
    12. upfval2
    13. upfval3
    14. isuplem
    15. isup
    16. uppropd
    17. reldmup2
    18. relup
    19. uprcl
    20. up1st2nd
    21. up1st2ndr
    22. up1st2ndb
    23. up1st2nd2
    24. uprcl2
    25. uprcl3
    26. uprcl4
    27. uprcl5
    28. uobrcl
    29. isup2
    30. upeu3
    31. upeu4
    32. uptposlem
    33. uptpos
    34. oppcuprcl4
    35. oppcuprcl3
    36. oppcuprcl5
    37. oppcuprcl2
    38. uprcl2a
    39. oppfuprcl
    40. oppfuprcl2
    41. oppcup3lem
    42. oppcup
    43. oppcup2
    44. oppcup3
    45. uptrlem1
    46. uptrlem2
    47. uptrlem3
    48. uptr
    49. uptri
    50. uptra
    51. uptrar
    52. uptrai
    53. uobffth
    54. uobeqw
    55. uobeq
    56. uptr2
    57. uptr2a
11. Natural transformations and the functor category
    1. isnatd
    2. natrcl2
    3. natrcl3
    4. catbas
    5. cathomfval
    6. catcofval
    7. natoppf
    8. natoppf2
    9. natoppfb
12. Initial, terminal and zero objects of a category
    1. initoo2
    2. termoo2
    3. zeroo2
    4. oppcinito
    5. oppctermo
    6. oppczeroo
    7. termoeu2
    8. initopropdlemlem
    9. initopropdlem
    10. termopropdlem
    11. zeroopropdlem
    12. initopropd
    13. termopropd
    14. zeroopropd
13. Product of categories
    1. reldmxpc
    2. reldmxpcALT
    3. elxpcbasex1
    4. elxpcbasex1ALT
    5. elxpcbasex2
    6. elxpcbasex2ALT
    7. xpcfucbas
    8. xpcfuchomfval
    9. xpcfuchom
    10. xpcfuchom2
    11. xpcfucco2
    12. xpcfuccocl
    13. xpcfucco3
14. Swap functors
    1. cswapf
    2. df-swapf
    3. dfswapf2
    4. swapfval
    5. swapfelvv
    6. swapf2fvala
    7. swapf2fval
    8. swapf1vala
    9. swapf1val
    10. swapf2fn
    11. swapf1a
    12. swapf2vala
    13. swapf2a
    14. swapf1
    15. swapf2val
    16. swapf2
    17. swapf1f1o
    18. swapf2f1o
    19. swapf2f1oa
    20. swapf2f1oaALT
    21. swapfid
    22. swapfida
    23. swapfcoa
    24. swapffunc
    25. swapfffth
    26. swapffunca
    27. swapfiso
    28. swapciso
15. Functor evaluation
    1. oppc1stflem
    2. oppc1stf
    3. oppc2ndf
    4. 1stfpropd
    5. 2ndfpropd
    6. diagpropd
16. Transposed curry functors
    1. cofuswapfcl
    2. cofuswapf1
    3. cofuswapf2
    4. tposcurf1cl
    5. tposcurf11
    6. tposcurf12
    7. tposcurf1
    8. tposcurf2
    9. tposcurf2val
    10. tposcurf2cl
    11. tposcurfcl
17. Constant functors
    1. diag1
    2. diag1a
    3. diag1f1lem
    4. diag1f1
    5. diag2f1lem
    6. diag2f1
18. Functor composition bifunctors
    1. fucofulem1
    2. fucofulem2
    3. fuco2el
    4. fuco2eld
    5. fuco2eld2
    6. fuco2eld3
    7. cfuco
    8. df-fuco
    9. fucofvalg
    10. fucofval
    11. fucoelvv
    12. fuco1
    13. fucof1
    14. fuco2
    15. fucofn2
    16. fucofvalne
    17. fuco11
    18. fuco11cl
    19. fuco11a
    20. fuco112
    21. fuco111
    22. fuco111x
    23. fuco112x
    24. fuco112xa
    25. fuco11id
    26. fuco11idx
    27. fuco21
    28. fuco11b
    29. fuco11bALT
    30. fuco22
    31. fucofn22
    32. fuco23
    33. fuco22natlem1
    34. fuco22natlem2
    35. fuco22natlem3
    36. fuco22natlem
    37. fuco22nat
    38. fucof21
    39. fucoid
    40. fucoid2
    41. fuco22a
    42. fuco23alem
    43. fuco23a
    44. fucocolem1
    45. fucocolem2
    46. fucocolem3
    47. fucocolem4
    48. fucoco
    49. fucoco2
    50. fucofunc
    51. fucofunca
    52. fucolid
    53. fucorid
    54. fucorid2
19. Post-composition functors
    1. postcofval
    2. postcofcl
20. Pre-composition functors
    1. precofvallem
    2. precofval
    3. precofvalALT
    4. precofval2
    5. precofcl
    6. precofval3
    7. precoffunc
    8. cprcof
    9. df-prcof
    10. reldmprcof
    11. prcofvalg
    12. prcofvala
    13. prcofval
    14. prcofpropd
    15. prcofelvv
    16. reldmprcof1
    17. reldmprcof2
    18. prcoftposcurfuco
    19. prcoftposcurfucoa
    20. prcoffunc
    21. prcoffunca
    22. prcoffunca2
    23. prcof1
    24. prcof2a
    25. prcof2
    26. prcof21a
    27. prcof22a
    28. prcofdiag1
    29. prcofdiag