Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfdiag  Unicode version 
Description: Define the diagonal functor, which is the functor whose object part is . The value of the functor at an object is the constant functor which maps all objects in to and all morphisms to . The morphism part is a natural transformation between these functors, which takes to the natural transformation with every component equal to . (Contributed by Mario Carneiro, 6Jan2017.) 
Ref  Expression 

dfdiag  Δ_{func} curry_{F} _{F} 
Step  Hyp  Ref  Expression 

1  cdiag 14229  . 2 Δ_{func}  
2  vc  . . 3  
3  vd  . . 3  
4  ccat 13809  . . 3  
5  2  cv 1648  . . . . 5 
6  3  cv 1648  . . . . 5 
7  5, 6  cop 3753  . . . 4 
8  c1stf 14186  . . . . 5 _{F}  
9  5, 6, 8  co 6013  . . . 4 _{F} 
10  ccurf 14227  . . . 4 curry_{F}  
11  7, 9, 10  co 6013  . . 3 curry_{F} _{F} 
12  2, 3, 4, 4, 11  cmpt2 6015  . 2 curry_{F} _{F} 
13  1, 12  wceq 1649  1 Δ_{func} curry_{F} _{F} 
Colors of variables: wff set class 
This definition is referenced by: diagval 14257 
Copyright terms: Public domain  W3C validator 