Definition df-prstc

Description: Definition of the function converting a preordered set to a category. Justified by prsthinc .

This definition is somewhat arbitrary. Example 3.3(4.d) of Adamek p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism, by prstcnid , prstchom , and prstcthin . Other important properties include prstcbas , prstcleval , prstcle , prstcocval , prstcoc , prstchom2 , and prstcprs . Use those instead.

Note that the defining property prstchom is equivalent to prstchom2 given prstcthin . See thincn0eu for justification.

"ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Assertion	df-prstc	Could not format assertion : No typesetting found for |- ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprstc	Could not format ProsetToCat : No typesetting found for class ProsetToCat with typecode class
1		vk	$$setvark$$
2		cproset	$$class\mathrm{Proset}$$
3	1	cv	$$setvark$$
4		csts	$$class\mathrm{sSet}$$
5		chom	$$class\mathrm{Hom}$$
6		cnx	$$class\mathrm{ndx}$$
7	6 5	cfv	$$class\mathrm{Hom}\left(\mathrm{ndx}\right)$$
8		cple	$$class\mathrm{le}$$
9	3 8	cfv	$$class{\le }_k$$
10		c1o	$$class{1}_{𝑜}$$
11	10	csn	$$class\left\{1_{𝑜}\right\}$$
12	9 11	cxp	$$class\left({\le }_k\times \left\{1_{𝑜}\right\}\right)$$
13	7 12	cop	$$class⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_k\times \left\{1_{𝑜}\right\}⟩$$
14	3 13 4	co	$$class\left(k\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_k\times \left\{1_{𝑜}\right\}⟩\right)$$
15		cco	$$class\mathrm{comp}$$
16	6 15	cfv	$$class\mathrm{comp}\left(\mathrm{ndx}\right)$$
17		c0	$$class\varnothing$$
18	16 17	cop	$$class⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩$$
19	14 18 4	co	$$class\left(\left(k\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_k\times \left\{1_{𝑜}\right\}⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩\right)$$
20	1 2 19	cmpt	$$class\left(k\in \mathrm{Proset}⟼\left(k\mathrm{sSet}⟨\mathrm{Hom}\left(\mathrm{ndx}\right),{\le }_k\times \left\{1_{𝑜}\right\}⟩\right)\mathrm{sSet}⟨\mathrm{comp}\left(\mathrm{ndx}\right),\varnothing ⟩\right)$$
21	0 20	wceq	Could not format ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) : No typesetting found for wff ProsetToCat = ( k e. Proset |-> ( ( k sSet <. ( Hom ` ndx ) , ( ( le ` k ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) with typecode wff