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

Definition df-diag 14006
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.)
Assertion
Ref Expression
df-diag  |- Δfunc  =  ( c  e.  Cat ,  d  e. 
Cat  |->  ( <. c ,  d >. curryF  ( c  1stF  d )
) )
Distinct variable group:    c, d

Detailed syntax breakdown of Definition df-diag
StepHypRef Expression
1 cdiag 14002 . 2  class Δfunc
2 vc . . 3  set  c
3 vd . . 3  set  d
4 ccat 13582 . . 3  class  Cat
52cv 1631 . . . . 5  class  c
63cv 1631 . . . . 5  class  d
75, 6cop 3656 . . . 4  class  <. c ,  d >.
8 c1stf 13959 . . . . 5  class  1stF
95, 6, 8co 5874 . . . 4  class  ( c  1stF  d )
10 ccurf 14000 . . . 4  class curryF
117, 9, 10co 5874 . . 3  class  ( <.
c ,  d >. curryF  ( c  1stF  d ) )
122, 3, 4, 4, 11cmpt2 5876 . 2  class  ( c  e.  Cat ,  d  e.  Cat  |->  ( <.
c ,  d >. curryF  ( c  1stF  d ) ) )
131, 12wceq 1632 1  wff Δfunc  =  ( c  e.  Cat ,  d  e. 
Cat  |->  ( <. c ,  d >. curryF  ( c  1stF  d )
) )
Colors of variables: wff set class
This definition is referenced by:  diagval  14030
  Copyright terms: Public domain W3C validator