Definition df-diag

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	$$⊢{\Delta }_{\mathrm{func}}=\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼⟨c,d⟩{curry}_F\left(c{1^{st}}_{F}d\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdiag	$$class{\Delta }_{\mathrm{func}}$$
1		vc	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		vd	$$setvard$$
4	1	cv	$$setvarc$$
5	3	cv	$$setvard$$
6	4 5	cop	$$class⟨c,d⟩$$
7		ccurf	$$class{curry}_F$$
8		c1stf	$$class{1^{st}}_F$$
9	4 5 8	co	$$class\left(c{1^{st}}_{F}d\right)$$
10	6 9 7	co	$$class\left(⟨c,d⟩{curry}_F\left(c{1^{st}}_{F}d\right)\right)$$
11	1 3 2 2 10	cmpo	$$class\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼⟨c,d⟩{curry}_F\left(c{1^{st}}_{F}d\right)\right)$$
12	0 11	wceq	$$wff{\Delta }_{\mathrm{func}}=\left(c\in \mathrm{Cat},d\in \mathrm{Cat}⟼⟨c,d⟩{curry}_F\left(c{1^{st}}_{F}d\right)\right)$$