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 | |- -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 ) ) ) ) >. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cprcof | |- -o.F |
|
| 1 | vp | |- p |
|
| 2 | cvv | |- _V |
|
| 3 | vf | |- f |
|
| 4 | c1st | |- 1st |
|
| 5 | 1 | cv | |- p |
| 6 | 5 4 | cfv | |- ( 1st ` p ) |
| 7 | vd | |- d |
|
| 8 | c2nd | |- 2nd |
|
| 9 | 5 8 | cfv | |- ( 2nd ` p ) |
| 10 | ve | |- e |
|
| 11 | 7 | cv | |- d |
| 12 | cfunc | |- Func |
|
| 13 | 10 | cv | |- e |
| 14 | 11 13 12 | co | |- ( d Func e ) |
| 15 | vb | |- b |
|
| 16 | vk | |- k |
|
| 17 | 15 | cv | |- b |
| 18 | 16 | cv | |- k |
| 19 | ccofu | |- o.func |
|
| 20 | 3 | cv | |- f |
| 21 | 18 20 19 | co | |- ( k o.func f ) |
| 22 | 16 17 21 | cmpt | |- ( k e. b |-> ( k o.func f ) ) |
| 23 | vl | |- l |
|
| 24 | va | |- a |
|
| 25 | cnat | |- Nat |
|
| 26 | 11 13 25 | co | |- ( d Nat e ) |
| 27 | 23 | cv | |- l |
| 28 | 18 27 26 | co | |- ( k ( d Nat e ) l ) |
| 29 | 24 | cv | |- a |
| 30 | 20 4 | cfv | |- ( 1st ` f ) |
| 31 | 29 30 | ccom | |- ( a o. ( 1st ` f ) ) |
| 32 | 24 28 31 | cmpt | |- ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) |
| 33 | 16 23 17 17 32 | cmpo | |- ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) |
| 34 | 22 33 | cop | |- <. ( k e. b |-> ( k o.func f ) ) , ( k e. b , l e. b |-> ( a e. ( k ( d Nat e ) l ) |-> ( a o. ( 1st ` f ) ) ) ) >. |
| 35 | 15 14 34 | csb | |- [_ ( 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 ) ) ) ) >. |
| 36 | 10 9 35 | csb | |- [_ ( 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 ) ) ) ) >. |
| 37 | 7 6 36 | csb | |- [_ ( 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 ) ) ) ) >. |
| 38 | 1 3 2 2 37 | cmpo | |- ( 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 ) ) ) ) >. ) |
| 39 | 0 38 | wceq | |- -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 ) ) ) ) >. ) |