Skip to content

Issues: UniMath/agda-unimath

Beta
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

97 Open 80 Closed
97 Open 80 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 metric-spaces module metric-spaces
#1421 opened May 1, 2025 by malarbol
2 tasks
@malarbol
2
Update metric spaces table metric-spaces
#1420 opened Apr 29, 2025 by malarbol
8 tasks
@malarbol
5
Change symbol for similarity improve naming question Further information is requested
#1418 opened Apr 28, 2025 by fredrik-bakke
1
1
Remove "everything" entry point with Agda 2.8.0 repo-maintenance tooling
#1408 opened Apr 24, 2025 by fredrik-bakke
Metric spaces / real analysis metric-spaces real-numbers
#1401 opened Apr 9, 2025 by malarbol
9 of 24 tasks
@lowasser @malarbol
11
Concept macro with empty field should cause error bug Something isn't working CI tooling
#1390 opened Mar 31, 2025 by fredrik-bakke
Formalize the notion of density in a strict poset order-theory
#1386 opened Mar 26, 2025 by lowasser
3
Remove postulates computational-behavior experiment foundation refactoring
#1379 opened Mar 24, 2025 by fredrik-bakke
3 of 11 tasks
@fredrik-bakke
7
Reasoning syntax doesn't produce the expected result for relations which aren't strictly left unital bug Something isn't working foundation
#1369 opened Mar 17, 2025 by VojtechStep
Concept macro incompatible with inline latex? bug Something isn't working mathswitch tooling
#1362 opened Mar 12, 2025 by fredrik-bakke
Lebesgue spaces metric-spaces
#1360 opened Mar 7, 2025 by lowasser
3
Best practices: encapsulation documentation Improvements or additions to documentation enhancement New feature or request guides refactoring repo-maintenance
#1359 opened Mar 6, 2025 by lowasser
2
Complex numbers
#1358 opened Mar 3, 2025 by lowasser
1
Polynomials and formal power series commutative-algebra ring-theory
#1357 opened Mar 3, 2025 by lowasser
4
Real analysis: continuity real-numbers
#1355 opened Feb 28, 2025 by lowasser
2
Real analysis: basic power series real-numbers
#1354 opened Feb 28, 2025 by lowasser
8
Real multiplication real-numbers
#1353 opened Feb 28, 2025 by lowasser
1
Judgmental rational addition computational-behavior elementary-number-theory
#1340 opened Feb 21, 2025 by lowasser
8
Large groups group-theory
#1334 opened Feb 18, 2025 by lowasser
8
Syntax modules enhancement New feature or request experiment question Further information is requested
#1332 opened Feb 15, 2025 by fredrik-bakke
14
Type duality and polynomial functors foundation question Further information is requested
#1331 opened Feb 15, 2025 by ncfavier
@EgbertRijke
1
Formalize the smash product as a pushout of half-smash products formalization-target synthetic-homotopy-theory
#1326 opened Feb 14, 2025 by fredrik-bakke
Macro for users/contributors CI documentation Improvements or additions to documentation tooling
#1323 opened Feb 14, 2025 by fredrik-bakke
2
Enable --lossy-unification globally? question Further information is requested tooling
#1267 opened Feb 4, 2025 by fredrik-bakke
2
Target: apartness algebras and their antisubalgebras commutative-algebra group-theory ring-theory
#1239 opened Jan 21, 2025 by djspacewhale
2
ProTip! Find all open issues with in progress development work with linked:pr.