Skip to content

Issues: agda/cubical

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

Clear current search query, filters, and sorts
61 Open 182 Closed
61 Open 182 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

Schemes new content New mathematical content
#657 opened Dec 2, 2021 by FredericPaugam
12
Shrink the Prelude refactor Refactorings, e.g. renaming, moving, rearranging...
#389 opened Jul 16, 2020 by mortberg
@mortberg
Cubical.**.Foo should only import **.Foo.Base and **.Foo.Properties order Structuring, enforcing conventions, renaming, ...
#396 opened Aug 3, 2020 by Saizan
@felixwellen
Reorganize files and prove equivalences of the many types of integers and rationals good first issue Good for newcomers
#404 opened Aug 27, 2020 by mortberg
8
Suggestion for application of SIP new content New mathematical content
#454 opened Oct 15, 2020 by martinescardo
5
Stern-Brocot rationals new content New mathematical content
#477 opened Nov 17, 2020 by ayberkt
Use the ringsolver with variables in context
#521 opened Mar 12, 2021 by mzeuner
1
Unify the symbol for decidable equality and use instance arguments
#528 opened Mar 25, 2021 by L-TChen
Files should not import things public order Structuring, enforcing conventions, renaming, ...
#569 opened Jun 9, 2021 by mortberg
1
Define inequality spaces
#575 opened Jun 24, 2021 by ghost
Remove the makeX functions but keep the makeIsX
#598 opened Aug 23, 2021 by mortberg
4
Cohomology with dependent coefficients new content New mathematical content
#616 opened Nov 2, 2021 by felixwellen
2
Apply the SIP to categories new content New mathematical content
#279 opened Apr 13, 2020 by mortberg
Develop/implement consistent naming conventions for Categories and Algebra order Structuring, enforcing conventions, renaming, ...
#646 opened Nov 24, 2021 by barrettj12
3
Record naming conventions order Structuring, enforcing conventions, renaming, ...
#661 opened Dec 2, 2021 by barrettj12
bibtex citation for the library
#662 opened Dec 8, 2021 by mortberg
2
Transfer Group definitions to AbGroup order Structuring, enforcing conventions, renaming, ...
#663 opened Dec 9, 2021 by barrettj12
4
Develop theory of additive/abelian categories new content New mathematical content
#675 opened Dec 16, 2021 by barrettj12
6 tasks
2
Define (co)equalisers, pushouts new content New mathematical content
#677 opened Dec 17, 2021 by barrettj12
1
Reflection/Base.agda won't typecheck with latest agda version
#709 opened Jan 28, 2022 by antoinevanmuylder
/Functions/FunExtEquiv.agda Error: Warning "Could not Generate equivalence
#711 opened Jan 29, 2022 by morphismz
2
Library type-checking time
#748 opened Mar 27, 2022 by anuyts
3
Strict monoidal categories lack coherence laws
#753 opened Mar 29, 2022 by anuyts
Indexed datatype in definition of free categories.
#760 opened Apr 8, 2022 by marcinjangrzybowski
Release new version for agda 2.7
#1148 opened Aug 17, 2024 by felixwellen
ProTip! Find all open issues with in progress development work with linked:pr.