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

Definition df-diag 15359
 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 15355 . 2 Δfunc
2 vc . . 3
3 vd . . 3
4 ccat 14938 . . 3
52cv 1382 . . . . 5
63cv 1382 . . . . 5
75, 6cop 4020 . . . 4
8 c1stf 15312 . . . . 5 F
95, 6, 8co 6281 . . . 4 F
10 ccurf 15353 . . . 4 curryF
117, 9, 10co 6281 . . 3 curryF F
122, 3, 4, 4, 11cmpt2 6283 . 2 curryF F
131, 12wceq 1383 1 Δfunc curryF F
 Colors of variables: wff setvar class This definition is referenced by:  diagval  15383
 Copyright terms: Public domain W3C validator