search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
454 stars 139 forks source link

Almost the structure sheaf property #920

Closed mzeuner closed 2 years ago

mzeuner commented 2 years ago

This PR proves a generalization of the main result in Cubical.Algebra.CommRIng.Localisation.PullbackSquare. I don't want to remove the latter file just yet and do this in a later PR with a full proof of the sheaf property of the structure sheaf.

mzeuner commented 2 years ago

Should be ready for merging (once the checks have passed)