Skip to content

Issues: UniMath/agda-unimath

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
23 Open 3 Closed
23 Open 3 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

Prove uniqueness of homotopy and equivalence induction foundation good first issue Good for newcomers
#1123 opened Apr 20, 2024 by fredrik-bakke
The long exact sequence of homotopy groups good first issue Good for newcomers synthetic-homotopy-theory
#834 opened Oct 12, 2023 by fredrik-bakke
1 of 7 tasks
Define unlabeled rooted trees good first issue Good for newcomers univalent-combinatorics
#749 opened Sep 10, 2023 by fredrik-bakke
1 task
Define the predicate that f maps two different elements to the same value good first issue Good for newcomers univalent-combinatorics
#748 opened Sep 10, 2023 by fredrik-bakke
1 task
Open claims for partitions of finite types good first issue Good for newcomers univalent-combinatorics
#747 opened Sep 10, 2023 by fredrik-bakke
5 tasks
Show that the type of Ferrers diagrams of any finite type is π-finite good first issue Good for newcomers univalent-combinatorics
#746 opened Sep 10, 2023 by fredrik-bakke
1 task
Show that the number of decidable equivalence relations on a finite type is a Stirling number of the second kind good first issue Good for newcomers univalent-combinatorics
#745 opened Sep 10, 2023 by fredrik-bakke
1 task
Show that the map from a pointed k+1-element type to the complement of the point is an equivalence good first issue Good for newcomers univalent-combinatorics
#744 opened Sep 10, 2023 by fredrik-bakke
1 task
Open claims about 2-element types good first issue Good for newcomers univalent-combinatorics
#743 opened Sep 10, 2023 by fredrik-bakke
4 tasks
Define ℂP∞ as the 2-truncation of the 2-sphere good first issue Good for newcomers synthetic-homotopy-theory
#742 opened Sep 10, 2023 by fredrik-bakke
1 task
Define equivalences of unlabeled structures of a species good first issue Good for newcomers species
#741 opened Sep 10, 2023 by fredrik-bakke
1 task
Define unital algebras over a ring good first issue Good for newcomers ring-theory
#740 opened Sep 10, 2023 by fredrik-bakke
1 task
2
Open claims regarding modalities good first issue Good for newcomers orthogonal-factorization-systems
#739 opened Sep 10, 2023 by fredrik-bakke
2 tasks
Open claims about orthogonal factorization systems good first issue Good for newcomers orthogonal-factorization-systems
#738 opened Sep 10, 2023 by fredrik-bakke
2 tasks
Equivalent sets have isomorphic symmetric concrete groups good first issue Good for newcomers group-theory
#737 opened Sep 10, 2023 by fredrik-bakke
1 task
Equivalences of concrete groups are isomorphisms of concrete groups good first issue Good for newcomers group-theory
#736 opened Sep 10, 2023 by fredrik-bakke
1 task
Open claims about surjective maps foundation good first issue Good for newcomers
#735 opened Sep 10, 2023 by fredrik-bakke
2 tasks
Show that the type of partial elements is a directed complete poset foundation good first issue Good for newcomers
#734 opened Sep 10, 2023 by fredrik-bakke
1 task
Show that Connected-Map-Into-Truncated-Type l2 k l A is k - l - 2-truncated foundation good first issue Good for newcomers
#733 opened Sep 10, 2023 by fredrik-bakke
2 tasks
Define maximal ideals for rings and commutative rings commutative-algebra good first issue Good for newcomers ring-theory
#731 opened Sep 10, 2023 by fredrik-bakke
4 tasks
Clean up the universal property of the integers cleanup elementary-number-theory good first issue Good for newcomers structured-types
#713 opened Aug 27, 2023 by VojtechStep
Formalize asserted connections between postulates in design principles documentation Improvements or additions to documentation formalization-target foundation good first issue Good for newcomers group-theory synthetic-homotopy-theory
#637 opened Jun 4, 2023 by fredrik-bakke
3 tasks
Prove that the interval type 𝕀 with strict β-laws on point constructors implies function extensionality good first issue Good for newcomers synthetic-homotopy-theory
#515 opened Mar 17, 2023 by fredrik-bakke
ProTip! Mix and match filters to narrow down what you’re looking for.