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	Could not format assertion : No typesetting found for |- -o.F = ( p e. _V , f e. _V |-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprcof	Could not format -o.F : No typesetting found for class -o.F with typecode class
1		vp	$$setvarp$$
2		cvv	$$class\mathrm{V}$$
3		vf	$$setvarf$$
4		c1st	$$class{1}^{st}$$
5	1	cv	$$setvarp$$
6	5 4	cfv	$$class{1}^{st}\left(p\right)$$
7		vd	$$setvard$$
8		c2nd	$$class{2}^{nd}$$
9	5 8	cfv	$$class{2}^{nd}\left(p\right)$$
10		ve	$$setvare$$
11	7	cv	$$setvard$$
12		cfunc	$$class\mathrm{Func}$$
13	10	cv	$$setvare$$
14	11 13 12	co	$$class\left(d\mathrm{Func}e\right)$$
15		vb	$$setvarb$$
16		vk	$$setvark$$
17	15	cv	$$setvarb$$
18	16	cv	$$setvark$$
19		ccofu	$$class{\circ }_{\mathrm{func}}$$
20	3	cv	$$setvarf$$
21	18 20 19	co	$$class\left(k{\circ }_{\mathrm{func}}f\right)$$
22	16 17 21	cmpt	$$class\left(k\in b⟼k{\circ }_{\mathrm{func}}f\right)$$
23		vl	$$setvarl$$
24		va	$$setvara$$
25		cnat	$$class\mathrm{Nat}$$
26	11 13 25	co	$$class\left(d\mathrm{Nat}e\right)$$
27	23	cv	$$setvarl$$
28	18 27 26	co	$$class\left(k\left(d\mathrm{Nat}e\right)l\right)$$
29	24	cv	$$setvara$$
30	20 4	cfv	$$class{1}^{st}\left(f\right)$$
31	29 30	ccom	$$class\left(a\circ 1^{st}\left(f\right)\right)$$
32	24 28 31	cmpt	$$class\left(a\in \left(k\left(d\mathrm{Nat}e\right)l\right)⟼a\circ 1^{st}\left(f\right)\right)$$
33	16 23 17 17 32	cmpo	$$class\left(k\in b,l\in b⟼\left(a\in \left(k\left(d\mathrm{Nat}e\right)l\right)⟼a\circ 1^{st}\left(f\right)\right)\right)$$
34	22 33	cop	$$class⟨\left(k\in b⟼k{\circ }_{\mathrm{func}}f\right),\left(k\in b,l\in b⟼\left(a\in \left(k\left(d\mathrm{Nat}e\right)l\right)⟼a\circ 1^{st}\left(f\right)\right)\right)⟩$$
35	15 14 34	csb	$$class⦋\left(d\mathrm{Func}e\right)/b⦌⟨\left(k\in b⟼k{\circ }_{\mathrm{func}}f\right),\left(k\in b,l\in b⟼\left(a\in \left(k\left(d\mathrm{Nat}e\right)l\right)⟼a\circ 1^{st}\left(f\right)\right)\right)⟩$$
36	10 9 35	csb	$$class⦋2^{nd}\left(p\right)/e⦌⦋\left(d\mathrm{Func}e\right)/b⦌⟨\left(k\in b⟼k{\circ }_{\mathrm{func}}f\right),\left(k\in b,l\in b⟼\left(a\in \left(k\left(d\mathrm{Nat}e\right)l\right)⟼a\circ 1^{st}\left(f\right)\right)\right)⟩$$
37	7 6 36	csb	$$class⦋1^{st}\left(p\right)/d⦌⦋2^{nd}\left(p\right)/e⦌⦋\left(d\mathrm{Func}e\right)/b⦌⟨\left(k\in b⟼k{\circ }_{\mathrm{func}}f\right),\left(k\in b,l\in b⟼\left(a\in \left(k\left(d\mathrm{Nat}e\right)l\right)⟼a\circ 1^{st}\left(f\right)\right)\right)⟩$$
38	1 3 2 2 37	cmpo	$$class\left(p\in \mathrm{V},f\in \mathrm{V}⟼⦋1^{st}\left(p\right)/d⦌⦋2^{nd}\left(p\right)/e⦌⦋\left(d\mathrm{Func}e\right)/b⦌⟨\left(k\in b⟼k{\circ }_{\mathrm{func}}f\right),\left(k\in b,l\in b⟼\left(a\in \left(k\left(d\mathrm{Nat}e\right)l\right)⟼a\circ 1^{st}\left(f\right)\right)\right)⟩\right)$$
39	0 38	wceq	Could not format -o.F = ( p e. _V , f e. _V |-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. ) : No typesetting found for wff -o.F = ( p e. _V , f e. _V |-> [_ ( 1st ` p ) / d ]_ [_ ( 2nd ` p ) / e ]_ [_ ( d Func e ) / b ]_ <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. ) with typecode wff