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} = (c \in Cat, d \in Cat ⟼ ⟨c, d⟩ {curry}_{F} (c {1^{st}}_{F} d))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdiag	$class Δ_{func}$
1		vc	$setvar c$
2		ccat	$class Cat$
3		vd	$setvar d$
4	1	cv	$setvar c$
5	3	cv	$setvar d$
6	4 5	cop	$class ⟨c, d⟩$
7		ccurf	$class {curry}_{F}$
8		c1stf	$class {1^{st}}_{F}$
9	4 5 8	co	$class (c {1^{st}}_{F} d)$
10	6 9 7	co	$class (⟨c, d⟩ {curry}_{F} (c {1^{st}}_{F} d))$
11	1 3 2 2 10	cmpo	$class (c \in Cat, d \in Cat ⟼ ⟨c, d⟩ {curry}_{F} (c {1^{st}}_{F} d))$
12	0 11	wceq	$wff Δ_{func} = (c \in Cat, d \in Cat ⟼ ⟨c, d⟩ {curry}_{F} (c {1^{st}}_{F} d))$

Metamath Proof Explorer

Definition df-diag

Detailed syntax breakdown