Definition df-diag 17460

Description: Define the diagonal functor, which is the functor 𝐶⟶(𝐷 Func 𝐶) 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 1(𝑥). 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 = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑)))

Distinct variable group:   𝑐,𝑑

Detailed syntax breakdown of Definition df-diag

Step	Hyp	Ref	Expression
1		cdiag 17456	. 2 class Δfunc
2		vc	. . 3 setvar 𝑐
3		vd	. . 3 setvar 𝑑
4		ccat 16929	. . 3 class Cat
5	2	cv 1532	. . . . 5 class 𝑐
6	3	cv 1532	. . . . 5 class 𝑑
7	5, 6	cop 4567	. . . 4 class ⟨𝑐, 𝑑⟩
8		c1stf 17413	. . . . 5 class 1stF
9	5, 6, 8	co 7150	. . . 4 class (𝑐 1stF 𝑑)
10		ccurf 17454	. . . 4 class curryF
11	7, 9, 10	co 7150	. . 3 class (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑))
12	2, 3, 4, 4, 11	cmpo 7152	. 2 class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑)))
13	1, 12	wceq 1533	1 wff Δfunc = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑)))

This definition is referenced by:  diagval  17484