move SetoidRewrite to main library and other changes in preparation for diagram chasing #2334
Conversation
Before moving SetoidRewriting to WildCat folder, we make sure other files in the library don't Require the WildCat.v meta-file, so they won't indirectly get SetoidRewriting imported. This will make the library continue to build with Coq 8.20, and will also reduce unnecessary rebuilds. We also reduce the dependence on Pointed/ and Algebra/, as some of those files will indirectly depend on SetoidRewriting in a future commit.
jdchristensen
force-pushed
the
diagram-chase-pr
branch
from
9569b12 to
5ac04a3
Compare
|
Commit eight: add "From HoTT" to test file to make opam builds work Commit nine: add new files to WildCat.v meta-file |
|
@Alizter If you want to just review an initial segment of this sequence of commits, that's fine, and I can split the rest off. I included a lot, because the later commits show what the earlier work is used for, but I know it's a lot to digest, so I'm happy to split it up. (We also have noticed that some things in HomologicalAlgebra.v can be cleaned up, so you might choose to skip that commit if you want to wait for us to clean it up first.) Cc: @ThomatoTomato |
|
I'm happy with the first 4 commits, but I ran out of time to review the others. I also have had trouble following the material on regular categories since I needed to re-review my old notes to understand things. Could you split the 4 commits off and we can get those merged. Then try tacking each commit at a time? |
jdchristensen
force-pushed
the
diagram-chase-pr
branch
from
29746f6 to
e0e30a4
Compare
|
@Alizter Ok, I trimmed this down to what was in the first four commits, plus the fixes in the 8th, 9th and 10th commits. Then I squashed some things together to make it more logical. Can you please check that I didn't mess things up? I'm in an airport and it'll be a day or two before I can look at this again. I'll wait to make sure this is good before creating the next PR. Cc: @ThomatoTomato |
jdchristensen
changed the title
2 participants
This is a fairly big PR that contains most of the work @ThomatoTomato and I have done on diagram chasing. (But there's at least one more PR still, which will show that AbGroup satisfies the assumptions of our set-up.)
The commits mostly touch disjoint files, and so can be read individually or sequentially. But since it's large, it's probably best to read them sequentially, which gets the dependencies correct. The library builds after each commit, even with 8.20.
The first commit just fixes a missing #[export] on an instance.
The second commit reduces the use of the meta-files WildCat.v, AbGroups.v and Pointed.v. WildCat.v is now never used internally. This has been done so that the next commit builds with 8.20, but even after we move to >= 9.0, this commit is valuable, as it means that a large part of the library doesn't need to be rebuilt when a leaf file like HomologicalAlgebra.v is changed. Also, the parallelization of the build is better, which saves some time.
The third commit moves SetoidRewrite.v from contrib to theories/WildCat/SetoidRewrite.v, with the tests moving to tests/WildCat/SetoidRewrite.v. No changes were made besides imports. This file is very useful for the work in commits 5, 6 and 7.
The fourth commit just has some minor changes to ZeroGroupoid.v.
The fifth commit (AbEnriched.v) introduces wild categories enriched in abelian groups, where the abelian group structure laws only hold up to 2-cells.
The sixth commit (Regular.v) introduces IsRegular and IsAbRegular wild categories, the latter being a nice place in which to do diagram chasing. Regular.v has the key tactic which makes diagram chasing go through smoothly.
The seventh commit (HomologicalAlgebra.v) proves many diagram lemmas using this method.
Edit: two commits added, see below for descriptions.
Edit: reduced this PR to the first four commits, plus some later things related to those commits. The rest will come as separate PRs.