CharlesCNorton
CharlesCNorton
@jdchristensen Thank you very much! Yes I am planning on an update, though I'm worried getting Coq/HoTT updated and working on Windows might actually take more time than updating the...
@jdchristensen @Alizter Update complete! It now compiles on Coq 8.20.1 + HoTT 8.20. Only needed to change True → Unit and I → tt in 3 places. Much easier than...
@jdchristensen Sorry for adding more while you're reviewing! I added two sections that might be useful: 1. **Suspension Fixed Points** - Shows zero is always a fixed point (ΣX ≅...
Sounds good! I'll start on that and implement the style fixes as well.
New commit is preparation for section division before file division. Should have this completed soon.
@jdchristensen File split complete! I've broken up the monolith into modular files as requested.
@jdchristensen I defer entirely to your judgment on the organization. I'll provide the ordered file list with dependencies as requested.
Please forgive the presentation. I will also upload: 1. **ZeroObjects.v** - Requires: N/A 2. **ZeroMorphismLemmas.v** - Requires: ZeroObjects 3. **Biproducts.v** - Requires: ZeroObjects, ZeroMorphismLemmas 4. **AdditiveCategories.v** - Requires: ZeroObjects, ZeroMorphismLemmas,...
> I've now review ZeroObjects.v. I found lots of inefficient things. Is it possible for you to extrapolate from the comments I made on this file and improve other files...
> @CharlesCNorton ...maybe you can finish up ZeroObjects.v in a new PR that we'll polish and merge, and then do a PR for the next file, etc. That will also...