Definition df-fuco

Description: Definition of functor composition bifunctors. Given three categories C , D , and E , ( <. C , D >. o.F E ) is a functor from the product category of two categories of functors to a category of functors ( fucofunc ). The object part maps two functors to their composition ( fuco11 ). The morphism part defines the "composition" of two natural transformations ( fuco22 ) into another natural transformation ( fuco22nat ) such that a "cube-like" diagram commutes. The naturality property also gives an alternate definition ( fuco23a ). Note that such "composition" is different from fucco because they "compose" along different "axes". (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Assertion	df-fuco	Could not format assertion : No typesetting found for |- o.F = ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfuco	Could not format o.F : No typesetting found for class o.F with typecode class
1		vp	$$setvarp$$
2		cvv	$$class\mathrm{V}$$
3		ve	$$setvare$$
4		c1st	$$class{1}^{st}$$
5	1	cv	$$setvarp$$
6	5 4	cfv	$$class{1}^{st}\left(p\right)$$
7		vc	$$setvarc$$
8		c2nd	$$class{2}^{nd}$$
9	5 8	cfv	$$class{2}^{nd}\left(p\right)$$
10		vd	$$setvard$$
11	10	cv	$$setvard$$
12		cfunc	$$class\mathrm{Func}$$
13	3	cv	$$setvare$$
14	11 13 12	co	$$class\left(d\mathrm{Func}e\right)$$
15	7	cv	$$setvarc$$
16	15 11 12	co	$$class\left(c\mathrm{Func}d\right)$$
17	14 16	cxp	$$class\left(\left(d\mathrm{Func}e\right)\times \left(c\mathrm{Func}d\right)\right)$$
18		vw	$$setvarw$$
19		ccofu	$$class{\circ }_{\mathrm{func}}$$
20	18	cv	$$setvarw$$
21	19 20	cres	$$class\left({{\circ }_{\mathrm{func}}\upharpoonright }_w\right)$$
22		vu	$$setvaru$$
23		vv	$$setvarv$$
24	22	cv	$$setvaru$$
25	24 8	cfv	$$class{2}^{nd}\left(u\right)$$
26	25 4	cfv	$$class{1}^{st}\left(2^{nd}\left(u\right)\right)$$
27		vf	$$setvarf$$
28	24 4	cfv	$$class{1}^{st}\left(u\right)$$
29	28 4	cfv	$$class{1}^{st}\left(1^{st}\left(u\right)\right)$$
30		vk	$$setvark$$
31	28 8	cfv	$$class{2}^{nd}\left(1^{st}\left(u\right)\right)$$
32		vl	$$setvarl$$
33	23	cv	$$setvarv$$
34	33 8	cfv	$$class{2}^{nd}\left(v\right)$$
35	34 4	cfv	$$class{1}^{st}\left(2^{nd}\left(v\right)\right)$$
36		vm	$$setvarm$$
37	33 4	cfv	$$class{1}^{st}\left(v\right)$$
38	37 4	cfv	$$class{1}^{st}\left(1^{st}\left(v\right)\right)$$
39		vr	$$setvarr$$
40		vb	$$setvarb$$
41		cnat	$$class\mathrm{Nat}$$
42	11 13 41	co	$$class\left(d\mathrm{Nat}e\right)$$
43	28 37 42	co	$$class\left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right)$$
44		va	$$setvara$$
45	15 11 41	co	$$class\left(c\mathrm{Nat}d\right)$$
46	25 34 45	co	$$class\left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)$$
47		vx	$$setvarx$$
48		cbs	$$class\mathrm{Base}$$
49	15 48	cfv	$$class{\mathrm{Base}}_c$$
50	40	cv	$$setvarb$$
51	36	cv	$$setvarm$$
52	47	cv	$$setvarx$$
53	52 51	cfv	$$classm\left(x\right)$$
54	53 50	cfv	$$classb\left(m\left(x\right)\right)$$
55	30	cv	$$setvark$$
56	27	cv	$$setvarf$$
57	52 56	cfv	$$classf\left(x\right)$$
58	57 55	cfv	$$classk\left(f\left(x\right)\right)$$
59	53 55	cfv	$$classk\left(m\left(x\right)\right)$$
60	58 59	cop	$$class⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩$$
61		cco	$$class\mathrm{comp}$$
62	13 61	cfv	$$class\mathrm{comp}\left(e\right)$$
63	39	cv	$$setvarr$$
64	53 63	cfv	$$classr\left(m\left(x\right)\right)$$
65	60 64 62	co	$$class\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)$$
66	32	cv	$$setvarl$$
67	57 53 66	co	$$class\left(f\left(x\right)lm\left(x\right)\right)$$
68	44	cv	$$setvara$$
69	52 68	cfv	$$classa\left(x\right)$$
70	69 67	cfv	$$class\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)$$
71	54 70 65	co	$$class\left(b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)$$
72	47 49 71	cmpt	$$class\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)$$
73	40 44 43 46 72	cmpo	$$class\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)$$
74	39 38 73	csb	$$class⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)$$
75	36 35 74	csb	$$class⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)$$
76	32 31 75	csb	$$class⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)$$
77	30 29 76	csb	$$class⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)$$
78	27 26 77	csb	$$class⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)$$
79	22 23 20 20 78	cmpo	$$class\left(u\in w,v\in w⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)$$
80	21 79	cop	$$class⟨{{\circ }_{\mathrm{func}}\upharpoonright }_w,\left(u\in w,v\in w⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩$$
81	18 17 80	csb	$$class⦋\left(\left(d\mathrm{Func}e\right)\times \left(c\mathrm{Func}d\right)\right)/w⦌⟨{{\circ }_{\mathrm{func}}\upharpoonright }_w,\left(u\in w,v\in w⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩$$
82	10 9 81	csb	$$class⦋2^{nd}\left(p\right)/d⦌⦋\left(\left(d\mathrm{Func}e\right)\times \left(c\mathrm{Func}d\right)\right)/w⦌⟨{{\circ }_{\mathrm{func}}\upharpoonright }_w,\left(u\in w,v\in w⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩$$
83	7 6 82	csb	$$class⦋1^{st}\left(p\right)/c⦌⦋2^{nd}\left(p\right)/d⦌⦋\left(\left(d\mathrm{Func}e\right)\times \left(c\mathrm{Func}d\right)\right)/w⦌⟨{{\circ }_{\mathrm{func}}\upharpoonright }_w,\left(u\in w,v\in w⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩$$
84	1 3 2 2 83	cmpo	$$class\left(p\in \mathrm{V},e\in \mathrm{V}⟼⦋1^{st}\left(p\right)/c⦌⦋2^{nd}\left(p\right)/d⦌⦋\left(\left(d\mathrm{Func}e\right)\times \left(c\mathrm{Func}d\right)\right)/w⦌⟨{{\circ }_{\mathrm{func}}\upharpoonright }_w,\left(u\in w,v\in w⟼⦋1^{st}\left(2^{nd}\left(u\right)\right)/f⦌⦋1^{st}\left(1^{st}\left(u\right)\right)/k⦌⦋2^{nd}\left(1^{st}\left(u\right)\right)/l⦌⦋1^{st}\left(2^{nd}\left(v\right)\right)/m⦌⦋1^{st}\left(1^{st}\left(v\right)\right)/r⦌\left(b\in \left(1^{st}\left(u\right)\left(d\mathrm{Nat}e\right)1^{st}\left(v\right)\right),a\in \left(2^{nd}\left(u\right)\left(c\mathrm{Nat}d\right)2^{nd}\left(v\right)\right)⟼\left(x\in {\mathrm{Base}}_c⟼b\left(m\left(x\right)\right)\left(⟨k\left(f\left(x\right)\right),k\left(m\left(x\right)\right)⟩\mathrm{comp}\left(e\right)r\left(m\left(x\right)\right)\right)\left(f\left(x\right)lm\left(x\right)\right)\left(a\left(x\right)\right)\right)\right)\right)⟩\right)$$
85	0 84	wceq	Could not format o.F = ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) : No typesetting found for wff o.F = ( p e. _V , e e. _V |-> [_ ( 1st ` p ) / c ]_ [_ ( 2nd ` p ) / d ]_ [_ ( ( d Func e ) X. ( c Func d ) ) / w ]_ <. ( o.func |` w ) , ( u e. w , v e. w |-> [_ ( 1st ` ( 2nd ` u ) ) / f ]_ [_ ( 1st ` ( 1st ` u ) ) / k ]_ [_ ( 2nd ` ( 1st ` u ) ) / l ]_ [_ ( 1st ` ( 2nd ` v ) ) / m ]_ [_ ( 1st ` ( 1st ` v ) ) / r ]_ ( b e. ( ( 1st ` u ) ( d Nat e ) ( 1st ` v ) ) , a e. ( ( 2nd ` u ) ( c Nat d ) ( 2nd ` v ) ) |-> ( x e. ( Base ` c ) |-> ( ( b ` ( m ` x ) ) ( <. ( k ` ( f ` x ) ) , ( k ` ( m ` x ) ) >. ( comp ` e ) ( r ` ( m ` x ) ) ) ( ( ( f ` x ) l ( m ` x ) ) ` ( a ` x ) ) ) ) ) ) >. ) with typecode wff