This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑑 ) ) )