Description: A changed natural transformation witnesses that post-composed functor composition has a different morphism part. (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 ) ) |
||
| fucoaltne.n | |- ( ph -> ( ( F ( 2nd ` K ) G ) ` A ) =/= A ) |
||
| Assertion | fucoaltne | |- ( ph -> ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) ) |
| 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 | fucoaltne.n | |- ( ph -> ( ( F ( 2nd ` K ) G ) ` A ) =/= A ) |
|
| 10 | eqid | |- ( ( C FuncCat E ) Xc. ( C FuncCat C ) ) = ( ( C FuncCat E ) Xc. ( C FuncCat C ) ) |
|
| 11 | eqid | |- ( idFunc ` C ) = ( idFunc ` C ) |
|
| 12 | eqid | |- ( Id ` ( C FuncCat C ) ) = ( Id ` ( C FuncCat C ) ) |
|
| 13 | 1 2 3 4 5 6 7 8 9 10 11 12 | fucoaltnelem | |- ( ph -> ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) ) |