Skip to content

Swap functors, transposed curry functors, post-composition functors, and pre-composition functors #5051

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 170 commits into from
Oct 17, 2025
Merged

Swap functors, transposed curry functors, post-composition functors, and pre-composition functors #5051

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
170 commits
Select commit Hold shift + click to select a range
07d7d4b
[add] assa2ass2; [shorten] assa2ass
zwang123 Sep 11, 2025
f3bbb42
[add] asclcom
zwang123 Sep 11, 2025
32c0f68
[add] elmgpcntrd
zwang123 Sep 11, 2025
23315ff
[prove] asclcntr; [add] asclelbas
zwang123 Sep 11, 2025
cd896ee
[minimize] asclcom
zwang123 Sep 11, 2025
1314c60
[delete] assascacom and assascacrng
zwang123 Sep 11, 2025
965747d
[improve] explanation of asclcom
zwang123 Sep 11, 2025
c24ecf9
[rename] structure map of associative algebra might be non-injective;…
zwang123 Sep 11, 2025
08e472b
[add] upcic (empty proof), upciclem1
zwang123 Sep 16, 2025
f43b615
[change] upciclem1: var change
zwang123 Sep 16, 2025
25c0084
[add] isisod; [prove] upcic; [propose] upciclem2; [move] reueqdv to main
zwang123 Sep 16, 2025
1994800
[add] funcrcl2, funcrcl3; [update] upcic, upciclem2
zwang123 Sep 17, 2025
d7d8534
[shorten] upcic with funcrcl2
zwang123 Sep 17, 2025
11cf071
[fix] functor
zwang123 Sep 17, 2025
5fb5705
[add] funcel1; [propose] funcel2
zwang123 Sep 17, 2025
f3d5e6c
Revert "[add] funcel1; [propose] funcel2"
zwang123 Sep 17, 2025
99ca29c
[prove] upciclem2
zwang123 Sep 17, 2025
281e9e2
[remove] upciclem2.n; [reformat] hypotheses; [trivial] formatting
zwang123 Sep 17, 2025
4d9a170
[trivial] formatting
zwang123 Sep 17, 2025
dcd187f
[add] a section for Universal property
zwang123 Sep 18, 2025
89447e9
[add] upeu
zwang123 Sep 19, 2025
83d5dc0
[fix] upeu description
zwang123 Sep 19, 2025
39d58c8
[add] upeu2lem, reuxfr1dd, upciclem2; [shorten] upciclem3; [propose] …
zwang123 Sep 19, 2025
869b159
[prove] upeu2
zwang123 Sep 19, 2025
2397a86
[move] reuxfr1dd; [fix] upciclem1 description
zwang123 Sep 20, 2025
bc35cc1
[move and fix] upeu2lem and description and line length
zwang123 Sep 20, 2025
b2d0871
Merge branch 'develop' into upcic
zwang123 Sep 20, 2025
c7d5ff6
[propose] oppgtoppc
zwang123 Sep 21, 2025
5c7cc39
[fix] oppgtoppc; [formatting]
zwang123 Sep 21, 2025
d70d546
[add] oppgoppchom
zwang123 Sep 21, 2025
737ef22
[add] oppgoppcco
zwang123 Sep 21, 2025
b7569f3
[add] oppgoppcid
zwang123 Sep 21, 2025
0b4c1d6
[add] oppgoppc comments; [fix] format
zwang123 Sep 22, 2025
b73bbcc
[add] thinccisod, oduoppcbas; [propose] oduoppcciso, oduoppc, oduoppccom
zwang123 Sep 22, 2025
161ed10
[move] oduprs from AV's mathbox to main
zwang123 Sep 22, 2025
28b800e
[prove] oduoppcciso
zwang123 Sep 22, 2025
4628495
Merge branch 'develop' into mndtc
zwang123 Sep 23, 2025
de1fa95
[add] upeu3
zwang123 Sep 24, 2025
1b6a262
[trivial] formatting
zwang123 Sep 24, 2025
70d0dbc
[move] reueqbidv to main; [trivial] formatting; [rename] isup, isup2;…
zwang123 Sep 24, 2025
35287f5
[add] oppcup; [fix] upfval2 hyp name
zwang123 Sep 24, 2025
ff879a2
[add] reldmup, uprcl1,2,3
zwang123 Sep 24, 2025
e0fd3f3
[add] relup
zwang123 Sep 24, 2025
7365137
[add] isuplem
zwang123 Sep 24, 2025
10cbbfe
[rm] hyp for isup2 and upeu3; [prove] uprcl4, uprcl5
zwang123 Sep 24, 2025
20e2634
[trivial] formatting
zwang123 Sep 24, 2025
1bfdfc6
[simplify] hyp for upeu3
zwang123 Sep 24, 2025
7484f6e
[add] upeu4
zwang123 Sep 25, 2025
0a0918b
[add] rescofuf
zwang123 Sep 25, 2025
939a477
[add] funcf2lem2, fucofulem1, fucofulem2
zwang123 Sep 26, 2025
62849d0
[shorten] funcf2lem2; [add] isnatd; [add] fuco
zwang123 Sep 29, 2025
94d30ed
[shorten]
zwang123 Sep 29, 2025
9986bed
[add] fmpod, fuco11id, fucoid2, etc; [move] fuco2el*, fmpodg
zwang123 Sep 30, 2025
0af658b
[shorten]
zwang123 Sep 30, 2025
f63eb67
[remove] hypotheses; [add] natrcl2/3; [fix] descriptions
zwang123 Oct 1, 2025
ee3fd82
[shorten] fuco22
zwang123 Oct 1, 2025
bb208b7
[add] Product of categories; [fix] minor
zwang123 Oct 1, 2025
b5731fb
[add] xpcfuccocl fuco22v; [remove hyp] xpcfucco2/3; [add] elrel2
zwang123 Oct 1, 2025
6eeb1d9
[remove] elrel2; use 1st2ndbr instead
zwang123 Oct 1, 2025
6bf405a
[add] fuco11v1, fuco22elnat2, fucocolem0-3; [propose] fuco23v
zwang123 Oct 2, 2025
3982010
rename fuco22elnat to lemma and remove usage. regen discourage
zwang123 Oct 2, 2025
166aa86
minor adjustments; rename; remove trash
zwang123 Oct 3, 2025
eb05005
rename, propose
zwang123 Oct 3, 2025
c4f9ab0
rename, regen discouraged
zwang123 Oct 3, 2025
d928a16
[prove] fvco11?; [propose] fucofunc
zwang123 Oct 3, 2025
d9b28f9
[prove] fuco11idx, fuco23a
zwang123 Oct 3, 2025
f4432bf
rename, reorder fucocolem?
zwang123 Oct 3, 2025
55b5a59
[prove] fucoco; [reformat]
zwang123 Oct 3, 2025
ebcc00f
[prove] fucoco2
zwang123 Oct 3, 2025
d244f41
[fix] xpcfuc theorems
zwang123 Oct 3, 2025
2f25e1b
[prove] fucofunc
zwang123 Oct 3, 2025
b618680
[add] more descriptions
zwang123 Oct 3, 2025
feca3ae
[minimize] fuco theorems
zwang123 Oct 4, 2025
59e0df7
[reorder] [collapse common hyp]
zwang123 Oct 4, 2025
03496e2
[reorder] fuco21; [fix] descriptions for fuco22natlem*
zwang123 Oct 4, 2025
3d14fd6
[remove] duplicate $d
zwang123 Oct 4, 2025
c230e82
[remove] duplicate hyp
zwang123 Oct 4, 2025
51b42c3
[remove] redundant $d
zwang123 Oct 4, 2025
b14ec6d
[remove] redundant $e
zwang123 Oct 4, 2025
8ba30b4
[add] $d; [fix] format
zwang123 Oct 4, 2025
3f0d861
reorder hyp
zwang123 Oct 4, 2025
d325d58
[add] $d and descriptions for fucofunc; [remove] dup hyp
zwang123 Oct 4, 2025
ed0e1c7
[remove] fucoeu; [reformat]
zwang123 Oct 4, 2025
1123014
[fix] descriptions
zwang123 Oct 4, 2025
fa6b2db
[update] discouraged
zwang123 Oct 5, 2025
8c1b518
Merge develop into fucofu and resolve merge conflict
zwang123 Oct 5, 2025
634ac5c
[fix] description of fucofunc
zwang123 Oct 5, 2025
2e186e9
[propose] df-swapf
zwang123 Oct 5, 2025
ce30f3c
[add] tposf1o-tposidf1o
zwang123 Oct 5, 2025
82b77be
[add] cosn, tposresxp
zwang123 Oct 6, 2025
b402cf8
[add] resinsnALT, tposideq
zwang123 Oct 6, 2025
af56eb8
[modify] tposideq2
zwang123 Oct 6, 2025
9e4779f
[fix] tposideq line length; [move] nel1nelin/nel2nelin to main
zwang123 Oct 6, 2025
cd78e77
[temp] remove unfinished work
zwang123 Oct 6, 2025
53ed835
Revert "[temp] remove unfinished work"
zwang123 Oct 6, 2025
a0e9c03
[fix] descriptions of df-up/upeu3/oppcup
zwang123 Oct 6, 2025
5c64f8e
[fix] descriptions of UP
zwang123 Oct 6, 2025
6624a76
[fix] long lines
zwang123 Oct 6, 2025
f67fe27
[fix] further shorten lines
zwang123 Oct 6, 2025
7442c14
[add] fucofvalne
zwang123 Oct 7, 2025
4807e81
[shorten] proofs
zwang123 Oct 7, 2025
6ce22fa
[shorten] change fucofvalg and shorten
zwang123 Oct 7, 2025
609953a
[fix] chapter title: https://github.com/metamath/set.mm/pull/5037#dis…
zwang123 Oct 7, 2025
c26928e
[fix] descriptions for fuco
zwang123 Oct 7, 2025
8000132
Merge branch develop into 'fucofu' and resolve conflict
zwang123 Oct 7, 2025
65e057a
[add] swapf theorems
zwang123 Oct 7, 2025
bfecff9
[prove] swapfelvv
zwang123 Oct 7, 2025
2e4f05d
[rearrange] switch hyp order
zwang123 Oct 7, 2025
1526827
[prove] fval theorems
zwang123 Oct 7, 2025
293b621
[prove] swapf2fn; [reorder]
zwang123 Oct 7, 2025
e71202b
[prove] swapf1a
zwang123 Oct 7, 2025
6e87f42
[rename][rewrap] [add] swapf1
zwang123 Oct 7, 2025
00ab6aa
[prove] swapf2
zwang123 Oct 7, 2025
35c5918
[modify] swapf2a
zwang123 Oct 7, 2025
3535648
[modify] descriptions and dates
zwang123 Oct 7, 2025
663c6a1
[add] f1o theorems
zwang123 Oct 8, 2025
69d259f
[add] swapfid; [propose] swapfco
zwang123 Oct 8, 2025
0f65ba5
[reorder] hyp such that the following is possible: ( ph -> ( <. C , D…
zwang123 Oct 8, 2025
e959f54
[add] swapfida, swapfcoa, swapffunc, swapfffth, swapciso
zwang123 Oct 8, 2025
4613497
[remove] redundant hyp
zwang123 Oct 8, 2025
1015363
[reorder] hyp such that the following is possible: ( ph -> X = <. ( 1…
zwang123 Oct 8, 2025
aed47e3
[prove] dfswapf2
zwang123 Oct 8, 2025
9261335
[rm] trash
zwang123 Oct 8, 2025
460107b
[add] descriptions; [minimize] swapf
zwang123 Oct 9, 2025
3d85eac
[reorder]; [remove] duplicate hyp
zwang123 Oct 9, 2025
3f46a72
[fix] syntax; [remove] $d for swapf1-swapf2
zwang123 Oct 9, 2025
3e0a327
[reorder] theorem; [remove] $d for f1o
zwang123 Oct 9, 2025
68edd3e
[add] shortened swapf2f1oa
zwang123 Oct 9, 2025
a1c5e0a
[remove] dup hyp
zwang123 Oct 9, 2025
603e38e
[remove] dup $d
zwang123 Oct 9, 2025
416bd11
[move] theoreoms; [remove] dup hyp
zwang123 Oct 9, 2025
e48654e
[fix] hyp
zwang123 Oct 9, 2025
4ec3c89
[add] descriptions; [reformat]
zwang123 Oct 9, 2025
4872462
[add] descriptions; [reformat]; [fix] hyp names
zwang123 Oct 9, 2025
258d38f
[temp] delete unfinished contents
zwang123 Oct 9, 2025
3929aa4
Revert "[temp] delete unfinished contents"
zwang123 Oct 9, 2025
a9c1be5
[add] tposcurf1
zwang123 Oct 9, 2025
e7dc971
[prove] tposcurf2
zwang123 Oct 9, 2025
6e543a9
[add] cofuswapfcl; [shorten] tposcurf11/tposcurf12
zwang123 Oct 9, 2025
226c343
[shorten] with cofuswapfcl
zwang123 Oct 9, 2025
20399c2
[prove] tposcurf2val, tposcurf2cl
zwang123 Oct 9, 2025
3138eda
Merge branch 'develop' into fucofu
zwang123 Oct 10, 2025
6ef12a4
Merge branch 'fucofu' into swapf; and resolve conflicts; base commit:…
zwang123 Oct 10, 2025
2bb4737
[temp] remove unfinished sections
zwang123 Oct 10, 2025
29e8f7b
Revert "[temp] remove unfinished sections"
zwang123 Oct 10, 2025
9e9e42f
[add] fucofunca, precofvallem, precofval
zwang123 Oct 11, 2025
184da0f
[remove] trash
zwang123 Oct 11, 2025
842f874
[improve] precofval
zwang123 Oct 11, 2025
8a16bae
[add] precofcl, precofval2
zwang123 Oct 11, 2025
a7c4dcc
[remove] trash
zwang123 Oct 11, 2025
b657cfe
[add] precoffunc
zwang123 Oct 11, 2025
49d7998
[add] fuco11b; [propose] postcofval
zwang123 Oct 11, 2025
466b8a4
[add] fucolid; [add] fuco11b to df-fuco description; [propose] fucorid
zwang123 Oct 11, 2025
e66da7f
[alt proof] fucolid
zwang123 Oct 11, 2025
38295ff
Revert "[alt proof] fucolid"
zwang123 Oct 11, 2025
4e5dba6
[prove] fucorid
zwang123 Oct 11, 2025
bb58d1d
[alt proof] fucorid
zwang123 Oct 11, 2025
f8f8ced
Revert "[alt proof] fucorid"
zwang123 Oct 11, 2025
5c18fae
[add] fucorid2; [remove] dup hyp, trash
zwang123 Oct 11, 2025
817186d
[add] postcofval, postcofcl; [remove] unused hyp for tposcurf1cl
zwang123 Oct 11, 2025
5ba3d54
[minimize] precoffunc
zwang123 Oct 11, 2025
9e0bf30
[minimize] precofval
zwang123 Oct 11, 2025
edda40a
[fix] verify warnings
zwang123 Oct 11, 2025
46baf4d
[fix] verify warnings
zwang123 Oct 11, 2025
45eea6e
[add] discouraged
zwang123 Oct 11, 2025
1122942
Merge branch 'develop' into swapf; and resolve conflicts
zwang123 Oct 12, 2025
56a85f8
[fix] grammatical error: https://github.com/metamath/set.mm/pull/5051…
zwang123 Oct 15, 2025
fd0c62e
[add] descriptions for tposrescnv
zwang123 Oct 15, 2025
9ddfd9b
[shorten] use reldmxpc to shorten elxpcbasex1 and elxpcbasex2
zwang123 Oct 15, 2025
e4c20f4
[fix] Alternate proof for -> Alternate proof of
zwang123 Oct 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions changes-set.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,8 @@ make a github issue.)
DONE:
Date Old New Notes
7-Oct-25 tgioo4 [same] Moved from GS's mathbox to main set.mm
6-Oct-25 nel2nelin [same] Moved from GS's mathbox to main set.mm
6-Oct-25 nel1nelin [same] Moved from GS's mathbox to main set.mm
5-Oct-25 eliund [same] Moved from GS's mathbox to main set.mm
5-Oct-25 feq1dd [same] Moved from GS's mathbox to main set.mm
5-Oct-25 offvalfv [same] Moved from AV's mathbox to main set.mm
Expand Down
Loading