Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fuc Structured version   Unicode version

Definition df-fuc 14133
 Description: Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
Assertion
Ref Expression
df-fuc FuncCat Nat comp Nat Nat comp
Distinct variable group:   ,,,,,,,,

Detailed syntax breakdown of Definition df-fuc
StepHypRef Expression
1 cfuc 14131 . 2 FuncCat
2 vt . . 3
3 vu . . 3
4 ccat 13881 . . 3
5 cnx 13458 . . . . . 6
6 cbs 13461 . . . . . 6
75, 6cfv 5446 . . . . 5
82cv 1651 . . . . . 6
93cv 1651 . . . . . 6
10 cfunc 14043 . . . . . 6
118, 9, 10co 6073 . . . . 5
127, 11cop 3809 . . . 4
13 chom 13532 . . . . . 6
145, 13cfv 5446 . . . . 5
15 cnat 14130 . . . . . 6 Nat
168, 9, 15co 6073 . . . . 5 Nat
1714, 16cop 3809 . . . 4 Nat
18 cco 13533 . . . . . 6 comp
195, 18cfv 5446 . . . . 5 comp
20 vv . . . . . 6
21 vh . . . . . 6
2211, 11cxp 4868 . . . . . 6
23 vf . . . . . . 7
2420cv 1651 . . . . . . . 8
25 c1st 6339 . . . . . . . 8
2624, 25cfv 5446 . . . . . . 7
27 vg . . . . . . . 8
28 c2nd 6340 . . . . . . . . 9
2924, 28cfv 5446 . . . . . . . 8
30 vb . . . . . . . . 9
31 va . . . . . . . . 9
3227cv 1651 . . . . . . . . . 10
3321cv 1651 . . . . . . . . . 10
3432, 33, 16co 6073 . . . . . . . . 9 Nat
3523cv 1651 . . . . . . . . . 10
3635, 32, 16co 6073 . . . . . . . . 9 Nat
37 vx . . . . . . . . . 10
388, 6cfv 5446 . . . . . . . . . 10
3937cv 1651 . . . . . . . . . . . 12
4030cv 1651 . . . . . . . . . . . 12
4139, 40cfv 5446 . . . . . . . . . . 11
4231cv 1651 . . . . . . . . . . . 12
4339, 42cfv 5446 . . . . . . . . . . 11
4435, 25cfv 5446 . . . . . . . . . . . . . 14
4539, 44cfv 5446 . . . . . . . . . . . . 13
4632, 25cfv 5446 . . . . . . . . . . . . . 14
4739, 46cfv 5446 . . . . . . . . . . . . 13
4845, 47cop 3809 . . . . . . . . . . . 12
4933, 25cfv 5446 . . . . . . . . . . . . 13
5039, 49cfv 5446 . . . . . . . . . . . 12
519, 18cfv 5446 . . . . . . . . . . . 12 comp
5248, 50, 51co 6073 . . . . . . . . . . 11 comp
5341, 43, 52co 6073 . . . . . . . . . 10 comp
5437, 38, 53cmpt 4258 . . . . . . . . 9 comp
5530, 31, 34, 36, 54cmpt2 6075 . . . . . . . 8 Nat Nat comp
5627, 29, 55csb 3243 . . . . . . 7 Nat Nat comp
5723, 26, 56csb 3243 . . . . . 6 Nat Nat comp
5820, 21, 22, 11, 57cmpt2 6075 . . . . 5 Nat Nat comp
5919, 58cop 3809 . . . 4 comp Nat Nat comp
6012, 17, 59ctp 3808 . . 3 Nat comp Nat Nat comp
612, 3, 4, 4, 60cmpt2 6075 . 2 Nat comp Nat Nat comp
621, 61wceq 1652 1 FuncCat Nat comp Nat Nat comp
 Colors of variables: wff set class This definition is referenced by:  fnfuc  14134  fucval  14147
 Copyright terms: Public domain W3C validator