Simplify (and generalize) `invElPropElimN`

MatthiasHu commented 7 months ago

This PR slightly simplifies the proof of invElPropElimN in Cubical/Algebra/CommRing/Localisation/InvertingElements.agda and drops the unnecessary restriction to positive numbers (suc n).

This slightly simplifies two other things as well:

Replace suc n by n in the whole file Cubical/Algebra/CommRing/Localisation/Limit.agda.
Remove the separate treatment of the n = 0 case of isSheaf𝓞ᴮ in Cubical/Algebra/ZariskiLattice/StructureSheaf.agda.

Disclaimer: I did not read/understand all of the code in which I replaced (suc n) with n. :-) But it only makes all statements stronger as far as I can see.

[I found this potential for improvement while reviewing #1086, and that PR will also be slightly simplified by the changes proposed here.]

felixwellen commented 7 months ago

Nice - looks good to me. Maybe @mzeuner has something to say as well.

mzeuner commented 7 months ago

Amazing, I don't know how I convinced myself that invElPropElimN would not work for n = 0. I think this PR can be merged.

MatthiasHu commented 7 months ago

Ok, thanks. I hope it is ok if I merge this myself then.

agda / cubical

Simplify (and generalize) `invElPropElimN` #1102