Definition df-up

Description: Definition of the class of universal properties.

Given categories D and E , if F : D --> E is a functor and W an object of E , a universal pair from W to F is a pair <. X , M >. consisting of an object X of D and a morphism M : W --> F X of E , such that to every pair <. y , g >. with y an object of D and g : W --> F y a morphism of E , there is a unique morphism k : X --> y of D with F k .o. M = g . Such property is commonly referred to as a universal property. In our definition, it is denoted as X ( F ( D UP E ) W ) M .

Note that the universal pair is termed differently as "universal arrow" in p. 55 of Mac Lane, Saunders,Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 6 Oct 2025). Interestingly, the "universal arrow" is referring to the morphism M instead of the pair near the end of the same piece of the text, causing name collision. The name "universal arrow" is also adopted in papers such as https://arxiv.org/pdf/2212.08981 . Alternatively, the universal pair is called the "universal morphism" in Wikipedia ( https://en.wikipedia.org/wiki/Universal_property ) as well as published works, e.g., https://arxiv.org/pdf/2412.12179 . But the pair <. X , M >. should be named differently as the morphism M , and thus we call X theuniversal object, M theuniversal morphism, and <. X , M >. theuniversal pair.

Given its existence, such universal pair is essentially unique ( upeu3 ), and can be generated from an existing universal pair by isomorphisms ( upeu4 ). See also oppcup for the dual concept.

(Contributed by Zhi Wang, 24-Sep-2025)

	Ref	Expression
Assertion	df-up	Could not format assertion : No typesetting found for |- UP = ( d e. _V , e e. _V |-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cup	Could not format UP : No typesetting found for class UP with typecode class
1		vd	$$setvard$$
2		cvv	$$class\mathrm{V}$$
3		ve	$$setvare$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvard$$
6	5 4	cfv	$$class{\mathrm{Base}}_d$$
7		vb	$$setvarb$$
8	3	cv	$$setvare$$
9	8 4	cfv	$$class{\mathrm{Base}}_e$$
10		vc	$$setvarc$$
11		chom	$$class\mathrm{Hom}$$
12	5 11	cfv	$$class\mathrm{Hom}\left(d\right)$$
13		vh	$$setvarh$$
14	8 11	cfv	$$class\mathrm{Hom}\left(e\right)$$
15		vj	$$setvarj$$
16		cco	$$class\mathrm{comp}$$
17	8 16	cfv	$$class\mathrm{comp}\left(e\right)$$
18		vo	$$setvaro$$
19		vf	$$setvarf$$
20		cfunc	$$class\mathrm{Func}$$
21	5 8 20	co	$$class\left(d\mathrm{Func}e\right)$$
22		vw	$$setvarw$$
23	10	cv	$$setvarc$$
24		vx	$$setvarx$$
25		vm	$$setvarm$$
26	24	cv	$$setvarx$$
27	7	cv	$$setvarb$$
28	26 27	wcel	$$wffx\in b$$
29	25	cv	$$setvarm$$
30	22	cv	$$setvarw$$
31	15	cv	$$setvarj$$
32		c1st	$$class{1}^{st}$$
33	19	cv	$$setvarf$$
34	33 32	cfv	$$class{1}^{st}\left(f\right)$$
35	26 34	cfv	$$class{1}^{st}\left(f\right)\left(x\right)$$
36	30 35 31	co	$$class\left(wj{1}^{st}\left(f\right)\left(x\right)\right)$$
37	29 36	wcel	$$wffm\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)$$
38	28 37	wa	$$wff\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)$$
39		vy	$$setvary$$
40		vg	$$setvarg$$
41	39	cv	$$setvary$$
42	41 34	cfv	$$class{1}^{st}\left(f\right)\left(y\right)$$
43	30 42 31	co	$$class\left(wj{1}^{st}\left(f\right)\left(y\right)\right)$$
44		vk	$$setvark$$
45	13	cv	$$setvarh$$
46	26 41 45	co	$$class\left(xhy\right)$$
47	40	cv	$$setvarg$$
48		c2nd	$$class{2}^{nd}$$
49	33 48	cfv	$$class{2}^{nd}\left(f\right)$$
50	26 41 49	co	$$class\left(x{2}^{nd}\left(f\right)y\right)$$
51	44	cv	$$setvark$$
52	51 50	cfv	$$class\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)$$
53	30 35	cop	$$class⟨w,1^{st}\left(f\right)\left(x\right)⟩$$
54	18	cv	$$setvaro$$
55	53 42 54	co	$$class\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)$$
56	52 29 55	co	$$class\left(\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)$$
57	47 56	wceq	$$wffg=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m$$
58	57 44 46	wreu	$$wff\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m$$
59	58 40 43	wral	$$wff\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m$$
60	59 39 27	wral	$$wff\forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m$$
61	38 60	wa	$$wff\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)$$
62	61 24 25	copab	$$class\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}$$
63	19 22 21 23 62	cmpo	$$class\left(f\in \left(d\mathrm{Func}e\right),w\in c⟼\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}\right)$$
64	18 17 63	csb	$$class⦋\mathrm{comp}\left(e\right)/o⦌\left(f\in \left(d\mathrm{Func}e\right),w\in c⟼\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}\right)$$
65	15 14 64	csb	$$class⦋\mathrm{Hom}\left(e\right)/j⦌⦋\mathrm{comp}\left(e\right)/o⦌\left(f\in \left(d\mathrm{Func}e\right),w\in c⟼\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}\right)$$
66	13 12 65	csb	$$class⦋\mathrm{Hom}\left(d\right)/h⦌⦋\mathrm{Hom}\left(e\right)/j⦌⦋\mathrm{comp}\left(e\right)/o⦌\left(f\in \left(d\mathrm{Func}e\right),w\in c⟼\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}\right)$$
67	10 9 66	csb	$$class⦋{\mathrm{Base}}_e/c⦌⦋\mathrm{Hom}\left(d\right)/h⦌⦋\mathrm{Hom}\left(e\right)/j⦌⦋\mathrm{comp}\left(e\right)/o⦌\left(f\in \left(d\mathrm{Func}e\right),w\in c⟼\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}\right)$$
68	7 6 67	csb	$$class⦋{\mathrm{Base}}_d/b⦌⦋{\mathrm{Base}}_e/c⦌⦋\mathrm{Hom}\left(d\right)/h⦌⦋\mathrm{Hom}\left(e\right)/j⦌⦋\mathrm{comp}\left(e\right)/o⦌\left(f\in \left(d\mathrm{Func}e\right),w\in c⟼\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}\right)$$
69	1 3 2 2 68	cmpo	$$class\left(d\in \mathrm{V},e\in \mathrm{V}⟼⦋{\mathrm{Base}}_d/b⦌⦋{\mathrm{Base}}_e/c⦌⦋\mathrm{Hom}\left(d\right)/h⦌⦋\mathrm{Hom}\left(e\right)/j⦌⦋\mathrm{comp}\left(e\right)/o⦌\left(f\in \left(d\mathrm{Func}e\right),w\in c⟼\left\{⟨x,m⟩|\left(\left(x\in b\wedge m\in \left(wj{1}^{st}\left(f\right)\left(x\right)\right)\right)\wedge \forall y\in b\forall g\in \left(wj{1}^{st}\left(f\right)\left(y\right)\right)\exists !k\in \left(xhy\right)g=\left(x{2}^{nd}\left(f\right)y\right)\left(k\right)\left(⟨w,1^{st}\left(f\right)\left(x\right)⟩o{1}^{st}\left(f\right)\left(y\right)\right)m\right)\right\}\right)\right)$$
70	0 69	wceq	Could not format UP = ( d e. _V , e e. _V |-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) ) : No typesetting found for wff UP = ( d e. _V , e e. _V |-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) ) with typecode wff