Metamath Proof Explorer

Table of Contents - 8.4.2. Functor evaluation

1. cevlf
2. ccurf
3. cuncf
4. cdiag
5. df-evlf
6. df-curf
7. df-uncf
8. df-diag
9. evlfval
10. evlf2
11. evlf2val
12. evlf1
13. evlfcllem
14. evlfcl
15. curfval
16. curf1fval
17. curf1
18. curf11
19. curf12
20. curf1cl
21. curf2
22. curf2val
23. curf2cl
24. curfcl
25. curfpropd
26. uncfval
27. uncfcl
28. uncf1
29. uncf2
30. curfuncf
31. uncfcurf
32. diagval
33. diagcl
34. diag1cl
35. diag11
36. diag12
37. diag2
38. diag2cl
39. curf2ndf