Description: At a pair consisting of a natural transformation and the identity of the identity functor, post-composed functor composition acts by the post- composing functor on that natural transformation. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fucoaltfunc.q | |- Q = ( C FuncCat E ) |
|
| fucoaltval.l | |- L = ( <. C , C >. o.F E ) |
||
| fucoaltval.c | |- ( ph -> C e. Cat ) |
||
| fucoaltval.e | |- ( ph -> E e. Cat ) |
||
| fucoaltval.k | |- ( ph -> K e. ( Q Func Q ) ) |
||
| fucoaltval.f | |- ( ph -> F e. ( C Func E ) ) |
||
| fucoaltval.g | |- ( ph -> G e. ( C Func E ) ) |
||
| fucoaltval.a | |- ( ph -> A e. ( F ( C Nat E ) G ) ) |
||
| fucoaltval.i | |- I = ( idFunc ` C ) |
||
| fucoaltval.j | |- J = ( Id ` ( C FuncCat C ) ) |
||
| Assertion | fucoaltval | |- ( ph -> ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( ( F ( 2nd ` K ) G ) ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fucoaltfunc.q | |- Q = ( C FuncCat E ) |
|
| 2 | fucoaltval.l | |- L = ( <. C , C >. o.F E ) |
|
| 3 | fucoaltval.c | |- ( ph -> C e. Cat ) |
|
| 4 | fucoaltval.e | |- ( ph -> E e. Cat ) |
|
| 5 | fucoaltval.k | |- ( ph -> K e. ( Q Func Q ) ) |
|
| 6 | fucoaltval.f | |- ( ph -> F e. ( C Func E ) ) |
|
| 7 | fucoaltval.g | |- ( ph -> G e. ( C Func E ) ) |
|
| 8 | fucoaltval.a | |- ( ph -> A e. ( F ( C Nat E ) G ) ) |
|
| 9 | fucoaltval.i | |- I = ( idFunc ` C ) |
|
| 10 | fucoaltval.j | |- J = ( Id ` ( C FuncCat C ) ) |
|
| 11 | eqid | |- ( ( C FuncCat E ) Xc. ( C FuncCat C ) ) = ( ( C FuncCat E ) Xc. ( C FuncCat C ) ) |
|
| 12 | 1 2 3 4 5 6 7 8 9 10 11 | fucoaltvallem | |- ( ph -> ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( ( F ( 2nd ` K ) G ) ` A ) ) |