Skip to content

Issues: pufferffish/agda-symmetries

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.

Sign up for GitHub

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

19 Open 48 Closed
19 Open 48 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

refactor this since Sorted is a prop todo
#97 opened Sep 17, 2024 by github-actions bot
Prove freeness for SLists
#93 opened Mar 28, 2024 by vikraman
1
Prove freeness of Lists
#92 opened Mar 28, 2024 by vikraman
@pufferffish
Define the statements of the universal property for the specific groupoid structures
#91 opened Mar 28, 2024 by vikraman
1
write the eliminators for FreeSMon and prove them by pattern matching todo
#89 opened Mar 25, 2024 by github-actions bot
pentagon coherence for lists todo
#88 opened Mar 25, 2024 by github-actions bot
1
@pufferffish
1
write the eliminators for FreeMon and prove them by pattern matching todo
#87 opened Mar 25, 2024 by github-actions bot
coherences on top of signatures and equations todo
#86 opened Mar 25, 2024 by github-actions bot
Fix levels in Free so this isn't necessary todo
#72 opened Nov 6, 2023 by github-actions bot
Add ⊕ as a helper in Mon.Desc todo
#65 opened Oct 30, 2023 by github-actions bot
Cleanup this mess todo
#59 opened Oct 29, 2023 by github-actions bot
Prove natural numbers are free X-structures on Y proof
#58 opened Oct 25, 2023 by vikraman
Define free commutative rig (or semiring) enhancement New feature or request proof
#57 opened Oct 25, 2023 by vikraman
Develop some applications enhancement New feature or request priority:low proof question Further information is requested
#55 opened Oct 18, 2023 by vikraman
@vikraman @pufferffish
Write generic lemma about compatibility between lookup and sharp priority:low todo
#52 opened Oct 17, 2023 by github-actions bot
Free symmetric monoidal groupoid on groupoids priority:high
#43 opened Oct 12, 2023 by pufferffish
Move isOfHLevel from Free to struct and rename ext priority:low
#33 opened Oct 7, 2023 by pufferffish
1
2
Improve the interface for Free enhancement New feature or request priority:low proof
#29 opened Oct 4, 2023 by vikraman
1 of 2 tasks
1
Investigate a general definition for free structures enhancement New feature or request priority:low proof
#4 opened Sep 18, 2023 by pufferffish
2
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.