Definition df-func

Description: Function returning all the functors from a category t to a category u . Definition 3.17 of Adamek p. 29, and definition in Lang p. 62 ("covariant functor"). Intuitively a functor associates any morphism of t to a morphism of u , any object of t to an object of u , and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of t to an object of u we write it associates any identity of t to an identity of u which simplifies the definition. According to remark 3.19 in Adamek p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (Contributed by FL, 10-Feb-2008) (Revised by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	df-func	⊢ Func = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfunc	⊢ Func
1		vt	⊢ 𝑡
2		ccat	⊢ Cat
3		vu	⊢ 𝑢
4		vf	⊢ 𝑓
5		vg	⊢ 𝑔
6		cbs	⊢ Base
7	1	cv	⊢ 𝑡
8	7 6	cfv	⊢ ( Base ‘ 𝑡 )
9		vb	⊢ 𝑏
10	4	cv	⊢ 𝑓
11	9	cv	⊢ 𝑏
12	3	cv	⊢ 𝑢
13	12 6	cfv	⊢ ( Base ‘ 𝑢 )
14	11 13 10	wf	⊢ 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 )
15	5	cv	⊢ 𝑔
16		vz	⊢ 𝑧
17	11 11	cxp	⊢ ( 𝑏 × 𝑏 )
18		c1st	⊢ 1st
19	16	cv	⊢ 𝑧
20	19 18	cfv	⊢ ( 1st ‘ 𝑧 )
21	20 10	cfv	⊢ ( 𝑓 ‘ ( 1st ‘ 𝑧 ) )
22		chom	⊢ Hom
23	12 22	cfv	⊢ ( Hom ‘ 𝑢 )
24		c2nd	⊢ 2nd
25	19 24	cfv	⊢ ( 2nd ‘ 𝑧 )
26	25 10	cfv	⊢ ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) )
27	21 26 23	co	⊢ ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) )
28		cmap	⊢ ↑m
29	7 22	cfv	⊢ ( Hom ‘ 𝑡 )
30	19 29	cfv	⊢ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 )
31	27 30 28	co	⊢ ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) )
32	16 17 31	cixp	⊢ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) )
33	15 32	wcel	⊢ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) )
34		vx	⊢ 𝑥
35	34	cv	⊢ 𝑥
36	35 35 15	co	⊢ ( 𝑥 𝑔 𝑥 )
37		ccid	⊢ Id
38	7 37	cfv	⊢ ( Id ‘ 𝑡 )
39	35 38	cfv	⊢ ( ( Id ‘ 𝑡 ) ‘ 𝑥 )
40	39 36	cfv	⊢ ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) )
41	12 37	cfv	⊢ ( Id ‘ 𝑢 )
42	35 10	cfv	⊢ ( 𝑓 ‘ 𝑥 )
43	42 41	cfv	⊢ ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) )
44	40 43	wceq	⊢ ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) )
45		vy	⊢ 𝑦
46		vm	⊢ 𝑚
47	45	cv	⊢ 𝑦
48	35 47 29	co	⊢ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 )
49		vn	⊢ 𝑛
50	47 19 29	co	⊢ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 )
51	35 19 15	co	⊢ ( 𝑥 𝑔 𝑧 )
52	49	cv	⊢ 𝑛
53	35 47	cop	⊢ ⟨ 𝑥 , 𝑦 ⟩
54		cco	⊢ comp
55	7 54	cfv	⊢ ( comp ‘ 𝑡 )
56	53 19 55	co	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 )
57	46	cv	⊢ 𝑚
58	52 57 56	co	⊢ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 )
59	58 51	cfv	⊢ ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) )
60	47 19 15	co	⊢ ( 𝑦 𝑔 𝑧 )
61	52 60	cfv	⊢ ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 )
62	47 10	cfv	⊢ ( 𝑓 ‘ 𝑦 )
63	42 62	cop	⊢ ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩
64	12 54	cfv	⊢ ( comp ‘ 𝑢 )
65	19 10	cfv	⊢ ( 𝑓 ‘ 𝑧 )
66	63 65 64	co	⊢ ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) )
67	35 47 15	co	⊢ ( 𝑥 𝑔 𝑦 )
68	57 67	cfv	⊢ ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 )
69	61 68 66	co	⊢ ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) )
70	59 69	wceq	⊢ ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) )
71	70 49 50	wral	⊢ ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) )
72	71 46 48	wral	⊢ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) )
73	72 16 11	wral	⊢ ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) )
74	73 45 11	wral	⊢ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) )
75	44 74	wa	⊢ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) )
76	75 34 11	wral	⊢ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) )
77	14 33 76	w3a	⊢ ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
78	77 9 8	wsbc	⊢ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) )
79	78 4 5	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) }
80	1 3 2 2 79	cmpo	⊢ ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
81	0 80	wceq	⊢ Func = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )