Metamath Proof Explorer


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 = e V , f V 1 st e / c 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccurf class curry F
1 ve setvar e
2 cvv class V
3 vf setvar f
4 c1st class 1 st
5 1 cv setvar e
6 5 4 cfv class 1 st e
7 vc setvar c
8 c2nd class 2 nd
9 5 8 cfv class 2 nd e
10 vd setvar d
11 vx setvar x
12 cbs class Base
13 7 cv setvar c
14 13 12 cfv class Base c
15 vy setvar y
16 10 cv setvar d
17 16 12 cfv class Base d
18 11 cv setvar x
19 3 cv setvar f
20 19 4 cfv class 1 st f
21 15 cv setvar y
22 18 21 20 co class x 1 st f y
23 15 17 22 cmpt class y Base d x 1 st f y
24 vz setvar z
25 vg setvar g
26 chom class Hom
27 16 26 cfv class Hom d
28 24 cv setvar z
29 21 28 27 co class y Hom d z
30 ccid class Id
31 13 30 cfv class Id c
32 18 31 cfv class Id c x
33 18 21 cop class x y
34 19 8 cfv class 2 nd f
35 18 28 cop class x z
36 33 35 34 co class x y 2 nd f x z
37 25 cv setvar g
38 32 37 36 co class Id c x x y 2 nd f x z g
39 25 29 38 cmpt class g y Hom d z Id c x x y 2 nd f x z g
40 15 24 17 17 39 cmpo class y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g
41 23 40 cop class y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g
42 11 14 41 cmpt class x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g
43 13 26 cfv class Hom c
44 18 21 43 co class x Hom c y
45 21 28 cop class y z
46 35 45 34 co class x z 2 nd f y z
47 16 30 cfv class Id d
48 28 47 cfv class Id d z
49 37 48 46 co class g x z 2 nd f y z Id d z
50 24 17 49 cmpt class z Base d g x z 2 nd f y z Id d z
51 25 44 50 cmpt class g x Hom c y z Base d g x z 2 nd f y z Id d z
52 11 15 14 14 51 cmpo class x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z
53 42 52 cop class x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z
54 10 9 53 csb class 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z
55 7 6 54 csb class 1 st e / c 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z
56 1 3 2 2 55 cmpo class e V , f V 1 st e / c 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z
57 0 56 wceq wff curry F = e V , f V 1 st e / c 2 nd e / d x Base c y Base d x 1 st f y y Base d , z Base d g y Hom d z Id c x x y 2 nd f x z g x Base c , y Base c g x Hom c y z Base d g x z 2 nd f y z Id d z