Theorem fucofunc

Description: The functor composition bifunctor is a functor. See also fucofunca .

However, it is unlikely the unique functor compatible with the functor composition. As a counterexample, let C and D be terminal categories (categories of one object and one morphism, df-termc ), for example, ( SetCat1o ) (the trivial category, setc1oterm ), and E be a category with two objects equipped with only two non-identity morphisms f and g , pointing in the same direction. It is possible to map the ordered pair of natural transformations <. a , i >. , where a sends to f and i is the identity natural transformation, to the other natural transformation b sending to g , i.e., define the morphism part P such that ( a ( U P V ) i ) = b such that ( bX ) = g given hypotheses of fuco23 . Such construction should be provable as a functor.

Given any P , it is a morphism part of a functor compatible with the object part, i.e., the functor composition, i.e., the restriction of o.func , iff both of the following hold.

1. It has the same form as df-fuco up to fuco23 , but ( ( B ( U P V ) A )X ) might be mapped to a different morphism in category E . See fucofulem2 for some insights.

2. fuco22nat , fucoid , and fucoco are satisfied.

(Contributed by Zhi Wang, 3-Oct-2025)

	Ref	Expression
Hypotheses	fucoco2.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
	fucoco2.q	|- Q = ( C FuncCat E )
	fucoco2.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
	fucofunc.c	|- ( ph -> C e. Cat )
	fucofunc.d	|- ( ph -> D e. Cat )
	fucofunc.e	|- ( ph -> E e. Cat )
Assertion	fucofunc	|- ( ph -> O ( T Func Q ) P )

Proof

Step	Hyp	Ref	Expression
1		fucoco2.t	|- T = ( ( D FuncCat E ) Xc. ( C FuncCat D ) )
2		fucoco2.q	|- Q = ( C FuncCat E )
3		fucoco2.o	|- ( ph -> ( <. C , D >. o.F E ) = <. O , P >. )
4		fucofunc.c	|- ( ph -> C e. Cat )
5		fucofunc.d	|- ( ph -> D e. Cat )
6		fucofunc.e	|- ( ph -> E e. Cat )
7	1	xpcfucbas	|- ( ( D Func E ) X. ( C Func D ) ) = ( Base ` T )
8	2	fucbas	|- ( C Func E ) = ( Base ` Q )
9		eqid	|- ( Hom ` T ) = ( Hom ` T )
10		eqid	|- ( C Nat E ) = ( C Nat E )
11	2 10	fuchom	|- ( C Nat E ) = ( Hom ` Q )
12		eqid	|- ( Id ` T ) = ( Id ` T )
13		eqid	|- ( Id ` Q ) = ( Id ` Q )
14		eqid	|- ( comp ` T ) = ( comp ` T )
15		eqid	|- ( comp ` Q ) = ( comp ` Q )
16		eqid	|- ( D FuncCat E ) = ( D FuncCat E )
17	16 5 6	fuccat	|- ( ph -> ( D FuncCat E ) e. Cat )
18		eqid	|- ( C FuncCat D ) = ( C FuncCat D )
19	18 4 5	fuccat	|- ( ph -> ( C FuncCat D ) e. Cat )
20	1 17 19	xpccat	|- ( ph -> T e. Cat )
21	2 4 6	fuccat	|- ( ph -> Q e. Cat )
22		eqidd	|- ( ph -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
23	4 5 6 3 22	fucof1	|- ( ph -> O : ( ( D Func E ) X. ( C Func D ) ) --> ( C Func E ) )
24	4 5 6 3 22	fucofn2	|- ( ph -> P Fn ( ( ( D Func E ) X. ( C Func D ) ) X. ( ( D Func E ) X. ( C Func D ) ) ) )
25	3	adantr	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
26		eqidd	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
27		simprl	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> x e. ( ( D Func E ) X. ( C Func D ) ) )
28		simprr	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> y e. ( ( D Func E ) X. ( C Func D ) ) )
29	25 1 9 26 27 28	fucof21	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) ) ) -> ( x P y ) : ( x ( Hom ` T ) y ) --> ( ( O ` x ) ( C Nat E ) ( O ` y ) ) )
30	3	adantr	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
31		eqidd	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
32		simpr	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> x e. ( ( D Func E ) X. ( C Func D ) ) )
33	30 1 12 2 13 31 32	fucoid2	|- ( ( ph /\ x e. ( ( D Func E ) X. ( C Func D ) ) ) -> ( ( x P x ) ` ( ( Id ` T ) ` x ) ) = ( ( Id ` Q ) ` ( O ` x ) ) )
34	3	3ad2ant1	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( <. C , D >. o.F E ) = <. O , P >. )
35		eqidd	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( ( D Func E ) X. ( C Func D ) ) = ( ( D Func E ) X. ( C Func D ) ) )
36		simp21	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> x e. ( ( D Func E ) X. ( C Func D ) ) )
37		simp22	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> y e. ( ( D Func E ) X. ( C Func D ) ) )
38		simp23	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> z e. ( ( D Func E ) X. ( C Func D ) ) )
39		simp3l	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> m e. ( x ( Hom ` T ) y ) )
40		simp3r	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> n e. ( y ( Hom ` T ) z ) )
41	1 2 34 14 15 35 36 37 38 9 39 40	fucoco2	|- ( ( ph /\ ( x e. ( ( D Func E ) X. ( C Func D ) ) /\ y e. ( ( D Func E ) X. ( C Func D ) ) /\ z e. ( ( D Func E ) X. ( C Func D ) ) ) /\ ( m e. ( x ( Hom ` T ) y ) /\ n e. ( y ( Hom ` T ) z ) ) ) -> ( ( x P z ) ` ( n ( <. x , y >. ( comp ` T ) z ) m ) ) = ( ( ( y P z ) ` n ) ( <. ( O ` x ) , ( O ` y ) >. ( comp ` Q ) ( O ` z ) ) ( ( x P y ) ` m ) ) )
42	7 8 9 11 12 13 14 15 20 21 23 24 29 33 41	isfuncd	|- ( ph -> O ( T Func Q ) P )