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

Definition df-fuc 13834
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  =  ( t  e.  Cat ,  u  e.  Cat  |->  { <. (
Base `  ndx ) ,  ( t  Func  u
) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
Distinct variable group:    a, b, f, g, h, t, u, v, x

Detailed syntax breakdown of Definition df-fuc
StepHypRef Expression
1 cfuc 13832 . 2  class FuncCat
2 vt . . 3  set  t
3 vu . . 3  set  u
4 ccat 13582 . . 3  class  Cat
5 cnx 13161 . . . . . 6  class  ndx
6 cbs 13164 . . . . . 6  class  Base
75, 6cfv 5271 . . . . 5  class  ( Base `  ndx )
82cv 1631 . . . . . 6  class  t
93cv 1631 . . . . . 6  class  u
10 cfunc 13744 . . . . . 6  class  Func
118, 9, 10co 5874 . . . . 5  class  ( t 
Func  u )
127, 11cop 3656 . . . 4  class  <. ( Base `  ndx ) ,  ( t  Func  u
) >.
13 chom 13235 . . . . . 6  class  Hom
145, 13cfv 5271 . . . . 5  class  (  Hom  `  ndx )
15 cnat 13831 . . . . . 6  class Nat
168, 9, 15co 5874 . . . . 5  class  ( t Nat  u )
1714, 16cop 3656 . . . 4  class  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>.
18 cco 13236 . . . . . 6  class comp
195, 18cfv 5271 . . . . 5  class  (comp `  ndx )
20 vv . . . . . 6  set  v
21 vh . . . . . 6  set  h
2211, 11cxp 4703 . . . . . 6  class  ( ( t  Func  u )  X.  ( t  Func  u
) )
23 vf . . . . . . 7  set  f
2420cv 1631 . . . . . . . 8  class  v
25 c1st 6136 . . . . . . . 8  class  1st
2624, 25cfv 5271 . . . . . . 7  class  ( 1st `  v )
27 vg . . . . . . . 8  set  g
28 c2nd 6137 . . . . . . . . 9  class  2nd
2924, 28cfv 5271 . . . . . . . 8  class  ( 2nd `  v )
30 vb . . . . . . . . 9  set  b
31 va . . . . . . . . 9  set  a
3227cv 1631 . . . . . . . . . 10  class  g
3321cv 1631 . . . . . . . . . 10  class  h
3432, 33, 16co 5874 . . . . . . . . 9  class  ( g ( t Nat  u ) h )
3523cv 1631 . . . . . . . . . 10  class  f
3635, 32, 16co 5874 . . . . . . . . 9  class  ( f ( t Nat  u ) g )
37 vx . . . . . . . . . 10  set  x
388, 6cfv 5271 . . . . . . . . . 10  class  ( Base `  t )
3937cv 1631 . . . . . . . . . . . 12  class  x
4030cv 1631 . . . . . . . . . . . 12  class  b
4139, 40cfv 5271 . . . . . . . . . . 11  class  ( b `
 x )
4231cv 1631 . . . . . . . . . . . 12  class  a
4339, 42cfv 5271 . . . . . . . . . . 11  class  ( a `
 x )
4435, 25cfv 5271 . . . . . . . . . . . . . 14  class  ( 1st `  f )
4539, 44cfv 5271 . . . . . . . . . . . . 13  class  ( ( 1st `  f ) `
 x )
4632, 25cfv 5271 . . . . . . . . . . . . . 14  class  ( 1st `  g )
4739, 46cfv 5271 . . . . . . . . . . . . 13  class  ( ( 1st `  g ) `
 x )
4845, 47cop 3656 . . . . . . . . . . . 12  class  <. (
( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >.
4933, 25cfv 5271 . . . . . . . . . . . . 13  class  ( 1st `  h )
5039, 49cfv 5271 . . . . . . . . . . . 12  class  ( ( 1st `  h ) `
 x )
519, 18cfv 5271 . . . . . . . . . . . 12  class  (comp `  u )
5248, 50, 51co 5874 . . . . . . . . . . 11  class  ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) )
5341, 43, 52co 5874 . . . . . . . . . 10  class  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  u )
( ( 1st `  h
) `  x )
) ( a `  x ) )
5437, 38, 53cmpt 4093 . . . . . . . . 9  class  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) )
5530, 31, 34, 36, 54cmpt2 5876 . . . . . . . 8  class  ( b  e.  ( g ( t Nat  u ) h ) ,  a  e.  ( f ( t Nat  u ) g ) 
|->  ( x  e.  (
Base `  t )  |->  ( ( b `  x ) ( <.
( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )
5627, 29, 55csb 3094 . . . . . . 7  class  [_ ( 2nd `  v )  / 
g ]_ ( b  e.  ( g ( t Nat  u ) h ) ,  a  e.  ( f ( t Nat  u
) g )  |->  ( x  e.  ( Base `  t )  |->  ( ( b `  x ) ( <. ( ( 1st `  f ) `  x
) ,  ( ( 1st `  g ) `
 x ) >.
(comp `  u )
( ( 1st `  h
) `  x )
) ( a `  x ) ) ) )
5723, 26, 56csb 3094 . . . . . 6  class  [_ ( 1st `  v )  / 
f ]_ [_ ( 2nd `  v )  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) )
5820, 21, 22, 11, 57cmpt2 5876 . . . . 5  class  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) )
5919, 58cop 3656 . . . 4  class  <. (comp ` 
ndx ) ,  ( v  e.  ( ( t  Func  u )  X.  ( t  Func  u
) ) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >.
6012, 17, 59ctp 3655 . . 3  class  { <. (
Base `  ndx ) ,  ( t  Func  u
) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. }
612, 3, 4, 4, 60cmpt2 5876 . 2  class  ( t  e.  Cat ,  u  e.  Cat  |->  { <. ( Base `  ndx ) ,  ( t  Func  u
) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
621, 61wceq 1632 1  wff FuncCat  =  ( t  e.  Cat ,  u  e.  Cat  |->  { <. (
Base `  ndx ) ,  ( t  Func  u
) >. ,  <. (  Hom  `  ndx ) ,  ( t Nat  u )
>. ,  <. (comp `  ndx ) ,  ( v  e.  ( ( t 
Func  u )  X.  (
t  Func  u )
) ,  h  e.  ( t  Func  u
)  |->  [_ ( 1st `  v
)  /  f ]_ [_ ( 2nd `  v
)  /  g ]_ ( b  e.  ( g ( t Nat  u
) h ) ,  a  e.  ( f ( t Nat  u ) g )  |->  ( x  e.  ( Base `  t
)  |->  ( ( b `
 x ) (
<. ( ( 1st `  f
) `  x ) ,  ( ( 1st `  g ) `  x
) >. (comp `  u
) ( ( 1st `  h ) `  x
) ) ( a `
 x ) ) ) ) ) >. } )
Colors of variables: wff set class
This definition is referenced by:  fnfuc  13835  fucval  13848
  Copyright terms: Public domain W3C validator