Definition df-diag 16856

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

Step	Hyp	Ref	Expression
1		cdiag 16852	. 2 class Δfunc
2		vc	. . 3 setvar c
3		vd	. . 3 setvar d
4		ccat 16325	. . 3 class Cat
5	2	cv 1482	. . . . 5 class c
6	3	cv 1482	. . . . 5 class d
7	5, 6	cop 4183	. . . 4 class <. c , d >.
8		c1stf 16809	. . . . 5 class 1stF
9	5, 6, 8	co 6650	. . . 4 class ( c 1stF d )
10		ccurf 16850	. . . 4 class curryF
11	7, 9, 10	co 6650	. . 3 class ( <. c , d >. curryF ( c 1stF d ) )
12	2, 3, 4, 4, 11	cmpt2 6652	. 2 class ( c e. Cat , d e. Cat |-> ( <. c , d >. curryF ( c 1stF d ) ) )
13	1, 12	wceq 1483	1 wff Δfunc = ( c e. Cat , d e. Cat |-> ( <. c , d >. curryF ( c 1stF d ) ) )

This definition is referenced by:  diagval  16880