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 | ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 ) | |
diagval.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | ||
diagval.d | ⊢ ( 𝜑 → 𝐷 ∈ Cat ) | ||
diagcl.q | ⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 ) | ||
Assertion | diagcl | ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝑄 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | diagval.l | ⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 ) | |
2 | diagval.c | ⊢ ( 𝜑 → 𝐶 ∈ Cat ) | |
3 | diagval.d | ⊢ ( 𝜑 → 𝐷 ∈ Cat ) | |
4 | diagcl.q | ⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 ) | |
5 | 1 2 3 | diagval | ⊢ ( 𝜑 → 𝐿 = ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) ) |
6 | eqid | ⊢ ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) = ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) | |
7 | eqid | ⊢ ( 𝐶 ×c 𝐷 ) = ( 𝐶 ×c 𝐷 ) | |
8 | eqid | ⊢ ( 𝐶 1stF 𝐷 ) = ( 𝐶 1stF 𝐷 ) | |
9 | 7 2 3 8 | 1stfcl | ⊢ ( 𝜑 → ( 𝐶 1stF 𝐷 ) ∈ ( ( 𝐶 ×c 𝐷 ) Func 𝐶 ) ) |
10 | 6 4 2 3 9 | curfcl | ⊢ ( 𝜑 → ( 〈 𝐶 , 𝐷 〉 curryF ( 𝐶 1stF 𝐷 ) ) ∈ ( 𝐶 Func 𝑄 ) ) |
11 | 5 10 | eqeltrd | ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 Func 𝑄 ) ) |