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

Definition df-diag 16679
 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
StepHypRef Expression
1 cdiag 16675 . 2 class Δfunc
2 vc . . 3 setvar 𝑐
3 vd . . 3 setvar 𝑑
4 ccat 16148 . . 3 class Cat
52cv 1474 . . . . 5 class 𝑐
63cv 1474 . . . . 5 class 𝑑
75, 6cop 4131 . . . 4 class 𝑐, 𝑑
8 c1stf 16632 . . . . 5 class 1stF
95, 6, 8co 6549 . . . 4 class (𝑐 1stF 𝑑)
10 ccurf 16673 . . . 4 class curryF
117, 9, 10co 6549 . . 3 class (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑))
122, 3, 4, 4, 11cmpt2 6551 . 2 class (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑)))
131, 12wceq 1475 1 wff Δfunc = (𝑐 ∈ Cat, 𝑑 ∈ Cat ↦ (⟨𝑐, 𝑑⟩ curryF (𝑐 1stF 𝑑)))
 Colors of variables: wff setvar class This definition is referenced by:  diagval  16703
 Copyright terms: Public domain W3C validator