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 も見てみましょう。
初心者向け すべて
オープン すべて

誰かが対応中かもしれないイシューは最後に並べています。 すべて日付順に表示

  • Clean up Cubical.Categories.Yoneda
    オープン
    • 何か問題がありますか？
    refactor

    難易度 5/5 1週間以上 初心者へのやさしさ 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 件 ·

  • Rewrite category theory code to separate structure and properties
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 20/100

    agda/cubical#1267 · コメント 6 件 · リアクション 2 件 ·

  • 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 1週間以上 初心者へのやさしさ 35/100

    agda/cubical#1254 · コメント 1 件 · リアクション 1 件 ·

  • 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 1週間以上 初心者へのやさしさ 18/100

    agda/cubical#1236 · コメント 4 件 ·

  • Formalize 'Combinatorics of higher-categorical diagrams' by Amar Hadzihasanovic
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 20/100

    agda/cubical#1218 ·

  • Define ends and coends
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 25/100

    agda/cubical#1197 ·

  • Notice: (Future) improvement to Glue usability
    オープン
    • 何か問題がありますか？
    discuss

    難易度 4/5 3〜5日 初心者へのやさしさ 35/100

    agda/cubical#1190 · コメント 3 件 · リアクション 1 件 ·

  • Move `Cubical.Algebra.SymmetricGroup` to `Cubical.Algebra.Group.Instances.Symmetric`
    オープン
    • 何か問題がありますか？

    難易度 3/5 1〜2日 初心者へのやさしさ 35/100

    agda/cubical#1186 ·

  • Formalize Ordered CommRings
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 35/100

    agda/cubical#1181 · リアクション 3 件 ·

  • Formalizing Devalapurkar & Haine
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 25/100

    agda/cubical#1147 ·

  • Solver for wild categories
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 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 件 ·

  • 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 1週間以上 初心者へのやさしさ 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 件 ·

  • 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 1週間以上 初心者へのやさしさ 15/100

    agda/cubical#943 · コメント 2 件 ·

  • Where should I put stuffs about 2LTT?
    オープン
    • 何か問題がありますか？

    難易度 2/5 1〜3時間 初心者へのやさしさ 25/100

    agda/cubical#911 · リアクション 1 件 ·

  • Use 'assign' for PR management
    オープン
    • 何か問題がありますか？
    discuss

    難易度 2/5 1〜3時間 初心者へのやさしさ 38/100

    agda/cubical#905 · リアクション 1 件 ·

  • Short Names or Long Names?
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 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 1週間以上 初心者へのやさしさ 20/100

    agda/cubical#838 · コメント 1 件 ·

  • Rename Functions.FunExtEquiv to Functions.FunExt?
    オープン
    • 何か問題がありますか？
    order

    難易度 1/5 1時間未満 初心者へのやさしさ 38/100

    agda/cubical#835 · リアクション 1 件 ·

  • 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 1週間以上 初心者へのやさしさ 20/100

    agda/cubical#815 · コメント 5 件 ·

  • Splitting files in Algebra
    再び着手できるかも オープン
    • 何か問題がありますか？
    discuss

    agda/cubical#813 · コメント 13 件 · 担当者 1 名 ·

  • TypeCategory is strange
    オープン
    • 何か問題がありますか？

    難易度 5/5 1週間以上 初心者へのやさしさ 20/100

    agda/cubical#804 · コメント 1 件 ·

  • Naming conventions for category theory
    オープン
    • 何か問題がありますか？
    order

    難易度 5/5 1週間以上 初心者へのやさしさ 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 1週間以上 初心者へのやさしさ 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 1週間以上 初心者へのやさしさ 25/100

    agda/cubical#677 · コメント 1 件 ·

  • Develop theory of additive/abelian categories
    オープン
    • 何か問題がありますか？
    new content

    難易度 5/5 1週間以上 初心者へのやさしさ 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 件 ·

  • Record naming conventions
    オープン
    • 何か問題がありますか？
    order

    難易度 5/5 1週間以上 初心者へのやさしさ 25/100

    agda/cubical#661 ·

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。