Metamath Proof Explorer

Table of Contents - 8. BASIC CATEGORY THEORY

1. Categories
   1. Categories
   2. Opposite category
   3. Monomorphisms and epimorphisms
   4. Sections, inverses, isomorphisms
   5. Isomorphic objects
   6. Subcategories
   7. Functors
   8. Full & faithful functors
   9. Natural transformations and the functor category
   10. Initial, terminal and zero objects of a category
2. Arrows (disjointified hom-sets)
   1. cdoma
   2. ccoda
   3. carw
   4. choma
   5. df-doma
   6. df-coda
   7. df-homa
   8. df-arw
   9. homarcl
   10. homafval
   11. homaf
   12. homaval
   13. elhoma
   14. elhomai
   15. elhomai2
   16. homarcl2
   17. homarel
   18. homa1
   19. homahom2
   20. homahom
   21. homadm
   22. homacd
   23. homadmcd
   24. arwval
   25. arwrcl
   26. arwhoma
   27. homarw
   28. arwdm
   29. arwcd
   30. dmaf
   31. cdaf
   32. arwhom
   33. arwdmcd
   34. Identity and composition for arrows
3. Examples of categories
   1. The category of sets
   2. The category of categories
   3. The category of extensible structures
4. Categorical constructions
   1. Product of categories
   2. Functor evaluation
   3. Hom functor