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 = (t \in Cat, u \in Cat ⟼ \{⟨f, g⟩ \| \underset{˙}{[} {Base}_{t} / b \underset{˙}{]} (f : b ⟶ {Base}_{u} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)}) \land \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfunc	$class Func$
1		vt	$setvar t$
2		ccat	$class Cat$
3		vu	$setvar u$
4		vf	$setvar f$
5		vg	$setvar g$
6		cbs	$class Base$
7	1	cv	$setvar t$
8	7 6	cfv	$class {Base}_{t}$
9		vb	$setvar b$
10	4	cv	$setvar f$
11	9	cv	$setvar b$
12	3	cv	$setvar u$
13	12 6	cfv	$class {Base}_{u}$
14	11 13 10	wf	$wff f : b ⟶ {Base}_{u}$
15	5	cv	$setvar g$
16		vz	$setvar z$
17	11 11	cxp	$class (b \times b)$
18		c1st	$class 1^{st}$
19	16	cv	$setvar z$
20	19 18	cfv	$class 1^{st} (z)$
21	20 10	cfv	$class f (1^{st} (z))$
22		chom	$class Hom$
23	12 22	cfv	$class Hom (u)$
24		c2nd	$class 2^{nd}$
25	19 24	cfv	$class 2^{nd} (z)$
26	25 10	cfv	$class f (2^{nd} (z))$
27	21 26 23	co	$class (f (1^{st} (z)) Hom (u) f (2^{nd} (z)))$
28		cmap	$class ↑_{𝑚}$
29	7 22	cfv	$class Hom (t)$
30	19 29	cfv	$class Hom (t) (z)$
31	27 30 28	co	$class ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)})$
32	16 17 31	cixp	$class \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)})$
33	15 32	wcel	$wff g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)})$
34		vx	$setvar x$
35	34	cv	$setvar x$
36	35 35 15	co	$class (x g x)$
37		ccid	$class Id$
38	7 37	cfv	$class Id (t)$
39	35 38	cfv	$class Id (t) (x)$
40	39 36	cfv	$class (x g x) (Id (t) (x))$
41	12 37	cfv	$class Id (u)$
42	35 10	cfv	$class f (x)$
43	42 41	cfv	$class Id (u) (f (x))$
44	40 43	wceq	$wff (x g x) (Id (t) (x)) = Id (u) (f (x))$
45		vy	$setvar y$
46		vm	$setvar m$
47	45	cv	$setvar y$
48	35 47 29	co	$class (x Hom (t) y)$
49		vn	$setvar n$
50	47 19 29	co	$class (y Hom (t) z)$
51	35 19 15	co	$class (x g z)$
52	49	cv	$setvar n$
53	35 47	cop	$class ⟨x, y⟩$
54		cco	$class comp$
55	7 54	cfv	$class comp (t)$
56	53 19 55	co	$class (⟨x, y⟩ comp (t) z)$
57	46	cv	$setvar m$
58	52 57 56	co	$class (n (⟨x, y⟩ comp (t) z) m)$
59	58 51	cfv	$class (x g z) (n (⟨x, y⟩ comp (t) z) m)$
60	47 19 15	co	$class (y g z)$
61	52 60	cfv	$class (y g z) (n)$
62	47 10	cfv	$class f (y)$
63	42 62	cop	$class ⟨f (x), f (y)⟩$
64	12 54	cfv	$class comp (u)$
65	19 10	cfv	$class f (z)$
66	63 65 64	co	$class (⟨f (x), f (y)⟩ comp (u) f (z))$
67	35 47 15	co	$class (x g y)$
68	57 67	cfv	$class (x g y) (m)$
69	61 68 66	co	$class ((y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m))$
70	59 69	wceq	$wff (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)$
71	70 49 50	wral	$wff \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)$
72	71 46 48	wral	$wff \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)$
73	72 16 11	wral	$wff \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)$
74	73 45 11	wral	$wff \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)$
75	44 74	wa	$wff ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m))$
76	75 34 11	wral	$wff \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m))$
77	14 33 76	w3a	$wff (f : b ⟶ {Base}_{u} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)}) \land \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)))$
78	77 9 8	wsbc	$wff \underset{˙}{[} {Base}_{t} / b \underset{˙}{]} (f : b ⟶ {Base}_{u} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)}) \land \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)))$
79	78 4 5	copab	$class \{⟨f, g⟩ \| \underset{˙}{[} {Base}_{t} / b \underset{˙}{]} (f : b ⟶ {Base}_{u} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)}) \land \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)))\}$
80	1 3 2 2 79	cmpo	$class (t \in Cat, u \in Cat ⟼ \{⟨f, g⟩ \| \underset{˙}{[} {Base}_{t} / b \underset{˙}{]} (f : b ⟶ {Base}_{u} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)}) \land \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)))\})$
81	0 80	wceq	$wff Func = (t \in Cat, u \in Cat ⟼ \{⟨f, g⟩ \| \underset{˙}{[} {Base}_{t} / b \underset{˙}{]} (f : b ⟶ {Base}_{u} \land g \in \underset{z \in b \times b}{⨉} ({(f (1^{st} (z)) Hom (u) f (2^{nd} (z)))}^{Hom (t) (z)}) \land \forall x \in b ((x g x) (Id (t) (x)) = Id (u) (f (x)) \land \forall y \in b \forall z \in b \forall m \in (x Hom (t) y) \forall n \in (y Hom (t) z) (x g z) (n (⟨x, y⟩ comp (t) z) m) = (y g z) (n) (⟨f (x), f (y)⟩ comp (u) f (z)) (x g y) (m)))\})$

Metamath Proof Explorer

Definition df-func

Detailed syntax breakdown