Definition df-diag

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)

	Ref	Expression
Assertion	df-diag	⊢ Δfunc = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ( ⟨ 𝑐 , 𝑑 ⟩ curryF ( 𝑐 1stF 𝑑 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdiag	⊢ Δfunc
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vd	⊢ 𝑑
4	1	cv	⊢ 𝑐
5	3	cv	⊢ 𝑑
6	4 5	cop	⊢ ⟨ 𝑐 , 𝑑 ⟩
7		ccurf	⊢ curryF
8		c1stf	⊢ 1stF
9	4 5 8	co	⊢ ( 𝑐 1stF 𝑑 )
10	6 9 7	co	⊢ ( ⟨ 𝑐 , 𝑑 ⟩ curryF ( 𝑐 1stF 𝑑 ) )
11	1 3 2 2 10	cmpo	⊢ ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ( ⟨ 𝑐 , 𝑑 ⟩ curryF ( 𝑐 1stF 𝑑 ) ) )
12	0 11	wceq	⊢ Δfunc = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ( ⟨ 𝑐 , 𝑑 ⟩ curryF ( 𝑐 1stF 𝑑 ) ) )