Theorem diagcl

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{\Delta }_{\mathrm{func}}D$$
	diagval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diagval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	diagcl.q	$$⊢Q=D\mathrm{FuncCat}C$$
Assertion	diagcl	$$⊢\phi \to L\in \left(C\mathrm{Func}Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		diagval.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		diagval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		diagval.d	$$⊢\phi \to D\in \mathrm{Cat}$$
4		diagcl.q	$$⊢Q=D\mathrm{FuncCat}C$$
5	1 2 3	diagval	$$⊢\phi \to L=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
6		eqid	$$⊢⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)=⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)$$
7		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
8		eqid	$$⊢C{1^{st}}_{F}D=C{1^{st}}_{F}D$$
9	7 2 3 8	1stfcl	$$⊢\phi \to C{1^{st}}_{F}D\in \left(\left(C{\times }_{c}D\right)\mathrm{Func}C\right)$$
10	6 4 2 3 9	curfcl	$$⊢\phi \to ⟨C,D⟩{curry}_F\left(C{1^{st}}_{F}D\right)\in \left(C\mathrm{Func}Q\right)$$
11	5 10	eqeltrd	$$⊢\phi \to L\in \left(C\mathrm{Func}Q\right)$$