Definition df-curf

Description: Define the curry functor, which maps a functor F : C X. D --> E to curryF ( F ) : C --> ( D --> E ) . (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Assertion	df-curf	$$⊢{curry}_F=\left(e\in \mathrm{V},f\in \mathrm{V}⟼⦋1^{st}\left(e\right)/c⦌⦋2^{nd}\left(e\right)/d⦌⟨\left(x\in {\mathrm{Base}}_c⟼⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)\right)⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccurf	$$class{curry}_F$$
1		ve	$$setvare$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		c1st	$$class{1}^{st}$$
5	1	cv	$$setvare$$
6	5 4	cfv	$$class{1}^{st}\left(e\right)$$
7		vc	$$setvarc$$
8		c2nd	$$class{2}^{nd}$$
9	5 8	cfv	$$class{2}^{nd}\left(e\right)$$
10		vd	$$setvard$$
11		vx	$$setvarx$$
12		cbs	$$class\mathrm{Base}$$
13	7	cv	$$setvarc$$
14	13 12	cfv	$$class{\mathrm{Base}}_c$$
15		vy	$$setvary$$
16	10	cv	$$setvard$$
17	16 12	cfv	$$class{\mathrm{Base}}_d$$
18	11	cv	$$setvarx$$
19	3	cv	$$setvarf$$
20	19 4	cfv	$$class{1}^{st}\left(f\right)$$
21	15	cv	$$setvary$$
22	18 21 20	co	$$class\left(x{1}^{st}\left(f\right)y\right)$$
23	15 17 22	cmpt	$$class\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right)$$
24		vz	$$setvarz$$
25		vg	$$setvarg$$
26		chom	$$class\mathrm{Hom}$$
27	16 26	cfv	$$class\mathrm{Hom}\left(d\right)$$
28	24	cv	$$setvarz$$
29	21 28 27	co	$$class\left(y\mathrm{Hom}\left(d\right)z\right)$$
30		ccid	$$class\mathrm{Id}$$
31	13 30	cfv	$$class\mathrm{Id}\left(c\right)$$
32	18 31	cfv	$$class\mathrm{Id}\left(c\right)\left(x\right)$$
33	18 21	cop	$$class⟨x,y⟩$$
34	19 8	cfv	$$class{2}^{nd}\left(f\right)$$
35	18 28	cop	$$class⟨x,z⟩$$
36	33 35 34	co	$$class\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)$$
37	25	cv	$$setvarg$$
38	32 37 36	co	$$class\left(\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)$$
39	25 29 38	cmpt	$$class\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)$$
40	15 24 17 17 39	cmpo	$$class\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)$$
41	23 40	cop	$$class⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩$$
42	11 14 41	cmpt	$$class\left(x\in {\mathrm{Base}}_c⟼⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩\right)$$
43	13 26	cfv	$$class\mathrm{Hom}\left(c\right)$$
44	18 21 43	co	$$class\left(x\mathrm{Hom}\left(c\right)y\right)$$
45	21 28	cop	$$class⟨y,z⟩$$
46	35 45 34	co	$$class\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)$$
47	16 30	cfv	$$class\mathrm{Id}\left(d\right)$$
48	28 47	cfv	$$class\mathrm{Id}\left(d\right)\left(z\right)$$
49	37 48 46	co	$$class\left(g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)$$
50	24 17 49	cmpt	$$class\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)$$
51	25 44 50	cmpt	$$class\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)$$
52	11 15 14 14 51	cmpo	$$class\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)\right)$$
53	42 52	cop	$$class⟨\left(x\in {\mathrm{Base}}_c⟼⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)\right)⟩$$
54	10 9 53	csb	$$class⦋2^{nd}\left(e\right)/d⦌⟨\left(x\in {\mathrm{Base}}_c⟼⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)\right)⟩$$
55	7 6 54	csb	$$class⦋1^{st}\left(e\right)/c⦌⦋2^{nd}\left(e\right)/d⦌⟨\left(x\in {\mathrm{Base}}_c⟼⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)\right)⟩$$
56	1 3 2 2 55	cmpo	$$class\left(e\in \mathrm{V},f\in \mathrm{V}⟼⦋1^{st}\left(e\right)/c⦌⦋2^{nd}\left(e\right)/d⦌⟨\left(x\in {\mathrm{Base}}_c⟼⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)\right)⟩\right)$$
57	0 56	wceq	$$wff{curry}_F=\left(e\in \mathrm{V},f\in \mathrm{V}⟼⦋1^{st}\left(e\right)/c⦌⦋2^{nd}\left(e\right)/d⦌⟨\left(x\in {\mathrm{Base}}_c⟼⟨\left(y\in {\mathrm{Base}}_d⟼x{1}^{st}\left(f\right)y\right),\left(y\in {\mathrm{Base}}_d,z\in {\mathrm{Base}}_d⟼\left(g\in \left(y\mathrm{Hom}\left(d\right)z\right)⟼\mathrm{Id}\left(c\right)\left(x\right)\left(⟨x,y⟩2^{nd}\left(f\right)⟨x,z⟩\right)g\right)\right)⟩\right),\left(x\in {\mathrm{Base}}_c,y\in {\mathrm{Base}}_c⟼\left(g\in \left(x\mathrm{Hom}\left(c\right)y\right)⟼\left(z\in {\mathrm{Base}}_d⟼g\left(⟨x,z⟩2^{nd}\left(f\right)⟨y,z⟩\right)\mathrm{Id}\left(d\right)\left(z\right)\right)\right)\right)⟩\right)$$