agda/cubical

登录后关注 在 GitHub 查看

An experimental library for Cubical Agda

agda/cubical 对新手友好吗？

近期外部贡献者向 agda/cubical 提交的 PR 还不够多，暂时无法判断它们被合并的比例。 目前没有开放的新手友好 issue，下方列出了我们收录的该仓库的其他 issue。

星标
572
派生
173
开放的新手 issue
0
已索引 issue
66
主要语言
Agda
许可证
没有许可证数据
最近 GitHub push
2026年10月8日
最近索引
2026年10月28日
没有贡献指南
没有行为准则
新手标签
good first issue
30 天内没有已合并 PR

如何为 agda/cubical 做贡献

  1. 这个项目没有贡献指南，可以先读 README，再看几个最近合并的 PR，了解改动是怎么提交的。
  2. 关注这个仓库，有新的新手友好 issue 时就能知道；也可以看看下方的其他 issue。
适合新手 全部
未关闭 全部

可能已有人在做的 issue 排在最后。 全部按时间排序

  • Clean up Cubical.Categories.Yoneda
    未关闭
    • 哪里不对？
    refactor

    难度 5/5 一周以上 新手友好度 20/100

    agda/cubical#1285 · 2 条评论 ·

  • Refactor modules for better compatibility with Cubical without Glue
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#1282 · 1 条评论 · 3 个 reaction ·

  • Rewrite category theory code to separate structure and properties
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 20/100

    agda/cubical#1267 · 6 条评论 · 2 个 reaction ·

  • Merge Fin.Data and Fin.Data.Inductive
    未关闭
    • 哪里不对？
    good first issue refactor

    难度 4/5 3-5 天 新手友好度 15/100

    agda/cubical#1264 · 1 条评论 ·

  • Define based identity systems
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 35/100

    agda/cubical#1254 · 1 条评论 · 1 个 reaction ·

  • Redundancy between Displayed.Constructions.PropertyOver and Category.Constructions.FullSubcategory
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#1248 · 6 条评论 ·

  • The powerset is not universe polymorphic enough
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 18/100

    agda/cubical#1236 · 4 条评论 ·

  • Formalize 'Combinatorics of higher-categorical diagrams' by Amar Hadzihasanovic
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 20/100

    agda/cubical#1218 ·

  • Define ends and coends
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 25/100

    agda/cubical#1197 ·

  • Notice: (Future) improvement to Glue usability
    未关闭
    • 哪里不对？
    discuss

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#1190 · 3 条评论 · 1 个 reaction ·

  • Move `Cubical.Algebra.SymmetricGroup` to `Cubical.Algebra.Group.Instances.Symmetric`
    未关闭
    • 哪里不对？

    难度 3/5 1-2 天 新手友好度 35/100

    agda/cubical#1186 ·

  • Formalize Ordered CommRings
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 35/100

    agda/cubical#1181 · 3 个 reaction ·

  • Formalizing Devalapurkar & Haine
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 25/100

    agda/cubical#1147 ·

  • Solver for wild categories
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 25/100

    agda/cubical#1118 ·

  • Make the CommRingSolver work better with concrete rings
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 42/100

    agda/cubical#1101 ·

  • SumMap in Algebra.Ring.BigOps should come from Semirings /Monoids
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 38/100

    agda/cubical#1088 · 2 条评论 ·

  • Suggested heap size for CI
    未关闭
    • 哪里不对？

    难度 2/5 1-3 小时 新手友好度 35/100

    agda/cubical#1074 · 1 条评论 ·

  • Duplication of code in the library
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 25/100

    agda/cubical#1017 · 5 条评论 · 1 个 reaction ·

  • Where should `π₁(RP²)` be?
    未关闭
    • 哪里不对？
    question

    难度 2/5 1-3 小时 新手友好度 25/100

    agda/cubical#1016 · 1 条评论 ·

  • Suggestion: provide proof that set-coequalizers of finite sets are finite?
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 35/100

    agda/cubical#1004 · 2 条评论 ·

  • `RecordEquiv` reflection doesn't seem to handle implicit field arguments
    可能重新可做 未关闭
    • 哪里不对？

    agda/cubical#995 · 6 条评论 · 已指派 1 人 ·

  • Code for Data.Fin.Properties needs to migrate to Cubical.Nat.Properties/Order
    未关闭
    • 哪里不对？

    难度 4/5 1-2 天 新手友好度 25/100

    agda/cubical#978 ·

  • Consider caching Nix artifacts via Cachix
    未关闭
    • 哪里不对？

    难度 3/5 1-2 天 新手友好度 48/100

    agda/cubical#960 · 2 个 reaction ·

  • Move Properties of UnivariateList-Polynomials to CommRing
    未关闭
    • 哪里不对？
    discuss refactor

    难度 4/5 3-5 天 新手友好度 38/100

    agda/cubical#944 ·

  • Define Universal Property for Algebraic Structures
    未关闭
    • 哪里不对？
    discuss new content refactor

    难度 5/5 一周以上 新手友好度 15/100

    agda/cubical#943 · 2 条评论 ·

  • Where should I put stuffs about 2LTT?
    未关闭
    • 哪里不对？

    难度 2/5 1-3 小时 新手友好度 25/100

    agda/cubical#911 · 1 个 reaction ·

  • Use 'assign' for PR management
    未关闭
    • 哪里不对？
    discuss

    难度 2/5 1-3 小时 新手友好度 38/100

    agda/cubical#905 · 1 个 reaction ·

  • Short Names or Long Names?
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 30/100

    agda/cubical#844 · 5 条评论 ·

  • Agda Nat exports Unit somehow
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 25/100

    agda/cubical#840 · 5 条评论 ·

  • Refactor Int ?
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 20/100

    agda/cubical#838 · 1 条评论 ·

  • Rename Functions.FunExtEquiv to Functions.FunExt?
    未关闭
    • 哪里不对？
    order

    难度 1/5 1 小时以内 新手友好度 38/100

    agda/cubical#835 · 1 个 reaction ·

  • Duplication with agda-stdlib
    可能重新可做 未关闭
    • 哪里不对？

    agda/cubical#832 · 3 条评论 · 已指派 1 人 ·

  • Module and elim
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 30/100

    agda/cubical#822 · 1 条评论 ·

  • Comment on the relation of notions of field in constructive algebra
    未关闭
    • 哪里不对？
    documentation

    难度 2/5 1-3 小时 新手友好度 35/100

    agda/cubical#819 ·

  • Clean up Cubical
    未关闭
    • 哪里不对？
    discuss

    难度 5/5 一周以上 新手友好度 20/100

    agda/cubical#815 · 5 条评论 ·

  • Splitting files in Algebra
    可能重新可做 未关闭
    • 哪里不对？
    discuss

    agda/cubical#813 · 13 条评论 · 已指派 1 人 ·

  • TypeCategory is strange
    未关闭
    • 哪里不对？

    难度 5/5 一周以上 新手友好度 20/100

    agda/cubical#804 · 1 条评论 ·

  • Naming conventions for category theory
    未关闭
    • 哪里不对？
    order

    难度 5/5 一周以上 新手友好度 25/100

    agda/cubical#803 · 5 条评论 ·

  • Useless import and make
    未关闭
    • 哪里不对？
    refactor

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#795 · 2 条评论 ·

  • Addition on the integer is defined on the right and not on the left
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#785 ·

  • Move and clean stuff from AbGroup.Base
    未关闭
    • 哪里不对？
    order

    难度 5/5 一周以上 新手友好度 15/100

    agda/cubical#776 · 1 条评论 ·

  • Use the new MonoidSolver
    未关闭
    • 哪里不对？
    refactor

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#761 ·

  • Library type-checking time
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#748 · 3 条评论 ·

  • /Functions/FunExtEquiv.agda Error: Warning "Could not Generate equivalence
    未关闭
    • 哪里不对？

    难度 3/5 1-2 天 新手友好度 25/100

    agda/cubical#711 · 2 条评论 ·

  • Reflection/Base.agda won't typecheck with latest agda version
    未关闭
    • 哪里不对？

    难度 4/5 3-5 天 新手友好度 35/100

    agda/cubical#709 ·

  • Define (co)equalisers, pushouts
    未关闭
    • 哪里不对？
    new content

    难度 5/5 一周以上 新手友好度 25/100

    agda/cubical#677 · 1 条评论 ·

  • Develop theory of additive/abelian categories
    未关闭
    • 哪里不对？
    new content

    难度 5/5 一周以上 新手友好度 20/100

    agda/cubical#675 · 2 条评论 ·

  • Transfer `Group` definitions to `AbGroup`
    未关闭
    • 哪里不对？
    order

    难度 4/5 3-5 天 新手友好度 38/100

    agda/cubical#663 · 4 条评论 ·

  • bibtex citation for the library
    未关闭
    • 哪里不对？

    难度 1/5 1 小时以内 新手友好度 35/100

    agda/cubical#662 · 2 条评论 · 2 个 reaction ·

  • Record naming conventions
    未关闭
    • 哪里不对？
    order

    难度 5/5 一周以上 新手友好度 25/100

    agda/cubical#661 ·

把新 issue 发到你的邮箱

精选适合新手参与的 GitHub issue 摘要。