Closed mzeuner closed 5 months ago
I don't fully understand what happened to the commit history here. @mzeuner Did you rebase but then also merge? Because some commits (such as "cleanup affine scheme") appear twice now (as https://github.com/agda/cubical/pull/1086/commits/947871f71283f7ee0c910a0eb486611d605e07c7 and as https://github.com/agda/cubical/pull/1086/commits/f4f95b6bb9c6879248e0e13d5120e49880315421).
Github still shows 107 files changed. But when I look at the diff locally (git diff master FuncQCQSSchemes
) it looks good (4 files changed)!
I don't really understand how this happened either. I rebased onto master but then git wouldn't let me push the changes until I also did a merge. Now I don't know what to do tbh...
Ah, I see.
A rebase always necessitates a force push (git push -f ...
) instead of a normal push, because you are (intentionally) overwriting the history of the remote branch.
In this case I think it makes sense to reset your local branch to f4f95b6bb9c6879248e0e13d5120e49880315421 (dropping the merge commit) and then force push that state.
(General hint: you can use git log --graph --all
to get an overview of branches and their history.)
Ok, I reset to the commit before the merge and force-pushed, now everything looks much better. Thanks!
Ok, nice! I merge it.
This PR builds on (https://github.com/agda/cubical/pull/1082). It proves that the Zariski coverage on
CommRing^op
is subcanonical, i.e. that representables are Zariski sheaves. Quasi-compact, quasi-separated schemes are defined as Zariski sheaves that have a finite affine cover by compact open subfunctors. Subcanonicity is then used to show that affine schemes (i.e. representables) are qcqs-schemes.