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

Definition df-diag 14305
 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, 6-Jan-2017.)
Assertion
Ref Expression
df-diag Δfunc curryF F
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-diag
StepHypRef Expression
1 cdiag 14301 . 2 Δfunc
2 vc . . 3
3 vd . . 3
4 ccat 13881 . . 3
52cv 1651 . . . . 5
63cv 1651 . . . . 5
75, 6cop 3809 . . . 4
8 c1stf 14258 . . . . 5 F
95, 6, 8co 6073 . . . 4 F
10 ccurf 14299 . . . 4 curryF
117, 9, 10co 6073 . . 3 curryF F
122, 3, 4, 4, 11cmpt2 6075 . 2 curryF F
131, 12wceq 1652 1 Δfunc curryF F
 Colors of variables: wff set class This definition is referenced by:  diagval  14329
 Copyright terms: Public domain W3C validator