Definition df-prcof

Description: Definition of pre-composition functors. The object part of the pre-composition functor given by F pre-composes a functor with F ; the morphism part pre-composes a natural transformation with the object part of F , in terms of function composition. Comments before the definition in § 3 of Chapter X in p. 236 of Mac Lane, Saunders,Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 3 Nov 2025). The notation -o.F is inspired by this page: https://1lab.dev/Cat.Functor.Compose.html .

The pre-composition functor can also be defined as a transposed curry of the functor composition bifunctor ( precofval3 ). But such definition requires an explicit third category. prcoftposcurfuco and prcoftposcurfucoa prove the equivalence. (Contributed by Zhi Wang, 2-Nov-2025)

	Ref	Expression
Assertion	df-prcof	⊢ −∘F = ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprcof	⊢ −∘F
1		vp	⊢ 𝑝
2		cvv	⊢ V
3		vf	⊢ 𝑓
4		c1st	⊢ 1st
5	1	cv	⊢ 𝑝
6	5 4	cfv	⊢ ( 1st ‘ 𝑝 )
7		vd	⊢ 𝑑
8		c2nd	⊢ 2nd
9	5 8	cfv	⊢ ( 2nd ‘ 𝑝 )
10		ve	⊢ 𝑒
11	7	cv	⊢ 𝑑
12		cfunc	⊢ Func
13	10	cv	⊢ 𝑒
14	11 13 12	co	⊢ ( 𝑑 Func 𝑒 )
15		vb	⊢ 𝑏
16		vk	⊢ 𝑘
17	15	cv	⊢ 𝑏
18	16	cv	⊢ 𝑘
19		ccofu	⊢ ∘func
20	3	cv	⊢ 𝑓
21	18 20 19	co	⊢ ( 𝑘 ∘func 𝑓 )
22	16 17 21	cmpt	⊢ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) )
23		vl	⊢ 𝑙
24		va	⊢ 𝑎
25		cnat	⊢ Nat
26	11 13 25	co	⊢ ( 𝑑 Nat 𝑒 )
27	23	cv	⊢ 𝑙
28	18 27 26	co	⊢ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 )
29	24	cv	⊢ 𝑎
30	20 4	cfv	⊢ ( 1st ‘ 𝑓 )
31	29 30	ccom	⊢ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) )
32	24 28 31	cmpt	⊢ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) )
33	16 23 17 17 32	cmpo	⊢ ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) )
34	22 33	cop	⊢ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩
35	15 14 34	csb	⊢ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩
36	10 9 35	csb	⊢ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩
37	7 6 36	csb	⊢ ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩
38	1 3 2 2 37	cmpo	⊢ ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ )
39	0 38	wceq	⊢ −∘F = ( 𝑝 ∈ V , 𝑓 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑒 ⦌ ⦋ ( 𝑑 Func 𝑒 ) / 𝑏 ⦌ ⟨ ( 𝑘 ∈ 𝑏 ↦ ( 𝑘 ∘func 𝑓 ) ) , ( 𝑘 ∈ 𝑏 , 𝑙 ∈ 𝑏 ↦ ( 𝑎 ∈ ( 𝑘 ( 𝑑 Nat 𝑒 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝑓 ) ) ) ) ⟩ )