Description: The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor ( y e. D |-> X ) is a construction that is natural in X (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | diagval.l | |- L = ( C DiagFunc D ) |
|
| diagval.c | |- ( ph -> C e. Cat ) |
||
| diagval.d | |- ( ph -> D e. Cat ) |
||
| diagcl.q | |- Q = ( D FuncCat C ) |
||
| Assertion | diagcl | |- ( ph -> L e. ( C Func Q ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | diagval.l | |- L = ( C DiagFunc D ) |
|
| 2 | diagval.c | |- ( ph -> C e. Cat ) |
|
| 3 | diagval.d | |- ( ph -> D e. Cat ) |
|
| 4 | diagcl.q | |- Q = ( D FuncCat C ) |
|
| 5 | 1 2 3 | diagval | |- ( ph -> L = ( <. C , D >. curryF ( C 1stF D ) ) ) |
| 6 | eqid | |- ( <. C , D >. curryF ( C 1stF D ) ) = ( <. C , D >. curryF ( C 1stF D ) ) |
|
| 7 | eqid | |- ( C Xc. D ) = ( C Xc. D ) |
|
| 8 | eqid | |- ( C 1stF D ) = ( C 1stF D ) |
|
| 9 | 7 2 3 8 | 1stfcl | |- ( ph -> ( C 1stF D ) e. ( ( C Xc. D ) Func C ) ) |
| 10 | 6 4 2 3 9 | curfcl | |- ( ph -> ( <. C , D >. curryF ( C 1stF D ) ) e. ( C Func Q ) ) |
| 11 | 5 10 | eqeltrd | |- ( ph -> L e. ( C Func Q ) ) |