Description: Hom-sets of the constructed category are dependent on the preorder.
Note that prstchom.x and prstchom.y are redundant here due to our definition of ProsetToCat . However, this should not be assumed as it is definition-dependent. Therefore, the two hypotheses are added for explicitness. (Contributed by Zhi Wang, 20-Sep-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | prstcnid.c | No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- | |
prstcnid.k | |
||
prstchom.l | |
||
prstchom.e | |
||
prstchom.x | |
||
prstchom.y | |
||
Assertion | prstchom | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prstcnid.c | Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |- | |
2 | prstcnid.k | |
|
3 | prstchom.l | |
|
4 | prstchom.e | |
|
5 | prstchom.x | |
|
6 | prstchom.y | |
|
7 | 1 2 3 | prstchomval | |
8 | 4 7 | eqtr4d | |
9 | 1oex | |
|
10 | 9 | a1i | |
11 | 1n0 | |
|
12 | 11 | a1i | |
13 | 8 10 12 | fvconstrn0 | |