Description: Define the diagonal functor, which is the functor C --> ( D Func C ) whose object part is x e. C |-> ( y e. D |-> x ) . The value of the functor at an object x is the constant functor which maps all objects in D to x and all morphisms to 1 ( x ) . The morphism part is a natural transformation between these functors, which takes f : x --> y to the natural transformation with every component equal to f . (Contributed by Mario Carneiro, 6-Jan-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-diag | |- DiagFunc = ( c e. Cat , d e. Cat |-> ( <. c , d >. curryF ( c 1stF d ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cdiag | |- DiagFunc |
|
| 1 | vc | |- c |
|
| 2 | ccat | |- Cat |
|
| 3 | vd | |- d |
|
| 4 | 1 | cv | |- c |
| 5 | 3 | cv | |- d |
| 6 | 4 5 | cop | |- <. c , d >. |
| 7 | ccurf | |- curryF |
|
| 8 | c1stf | |- 1stF |
|
| 9 | 4 5 8 | co | |- ( c 1stF d ) |
| 10 | 6 9 7 | co | |- ( <. c , d >. curryF ( c 1stF d ) ) |
| 11 | 1 3 2 2 10 | cmpo | |- ( c e. Cat , d e. Cat |-> ( <. c , d >. curryF ( c 1stF d ) ) ) |
| 12 | 0 11 | wceq | |- DiagFunc = ( c e. Cat , d e. Cat |-> ( <. c , d >. curryF ( c 1stF d ) ) ) |