Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Algebraic geometry directory, take 2 #1121

Merged
merged 7 commits into from
Apr 16, 2024
Merged

Conversation

mzeuner
Copy link
Contributor

@mzeuner mzeuner commented Apr 11, 2024

Redoing #1100, which seemed easier than fixing all the merge conflicts...

@mortberg
Copy link
Collaborator

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

@mzeuner
Copy link
Contributor Author

mzeuner commented Apr 11, 2024

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

@felixwellen
Copy link
Collaborator

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
Copy link
Contributor Author

mzeuner commented Apr 12, 2024

Like so?

@felixwellen
Copy link
Collaborator

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

@mortberg
Copy link
Collaborator

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

Should we merge?

@mzeuner
Copy link
Contributor Author

mzeuner commented Apr 15, 2024

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

@mortberg mortberg merged commit 598dfa5 into agda:master Apr 16, 2024
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants