search

agda / cubical

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

Algebraic geometry directory, take 2 #1121

Closed mzeuner closed 3 months ago

mzeuner commented 3 months ago

Redoing https://github.com/agda/cubical/pull/1100, which seemed easier than fixing all the merge conflicts...

mortberg commented 3 months ago

Nice! Is this ready to be merged or do you want to make any more changes?

mzeuner commented 3 months ago

Maybe @MatthiasHu or @felixwellen have something the would like to add or change?

felixwellen commented 3 months ago

Nothing to add, looks good to me. If you constructed the category of ZFunctors, maybe you still want to keep an instance (which might be just a public import of the instance from Cubical.AlgebraicGeometry....) in Cubical.Categories?

mzeuner commented 3 months ago

Like so?

felixwellen commented 3 months ago

Yes, good! I think it is better to have more references when in doubt.

mortberg commented 3 months ago

Yes, good! I think it is better to have more references when in doubt.

Should we merge?

mzeuner commented 3 months ago

Fixed a technicality in the comments, should be good to merge now.