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
Definition of dirichlet series #626
Conversation
…verse.lagda.md. I have Dirichlet series for species of finite inhabited types and for species of types in subuniverses. I also defined the product for each of these series
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just some comments on spelling 🙂
src/species/dirichlet-series-species-of-finite-inhabited-types.lagda.md
Outdated
Show resolved
Hide resolved
src/species/dirichlet-series-species-of-finite-inhabited-types.lagda.md
Outdated
Show resolved
Hide resolved
src/species/dirichlet-series-species-of-finite-inhabited-types.lagda.md
Outdated
Show resolved
Hide resolved
src/species/dirichlet-series-species-of-finite-inhabited-types.lagda.md
Outdated
Show resolved
Hide resolved
src/species/dirichlet-series-species-of-finite-inhabited-types.lagda.md
Outdated
Show resolved
Hide resolved
src/species/dirichlet-series-species-of-types-in-subuniverses.lagda.md
Outdated
Show resolved
Hide resolved
src/species/products-dirichlet-series-species-of-finite-inhabited-types.lagda.md
Outdated
Show resolved
Hide resolved
src/species/products-dirichlet-series-species-of-types-in-subuniverses.lagda.md
Outdated
Show resolved
Hide resolved
Thank you for the review :) |
Alright, I don't have anything more to add at this point. I'll wait and see if Egbert has anything to add, but otherwise, it's good to merge I think. |
Nice, thank you :) . |
Thanks for the question. Ideally, you would branch from your current PR branch, and then rebase onto agda-unimath/master after this PR is merged, I think. However, this is tricky to do(read: I mess this up every time) so I'll do you a favour and merge this PR now. |
Thank you so much :) |
Excellent! I agree with the merge. Good work! |
This PR suffered from #595 |
I have cleaned the file
dirichlet-products-species-of-types-in-subuniverse.lagda.md
.I have defined Dirichlet series for species of finite inhabited types and for species of types in subuniverses.
I have also defined the product for each of these series