Issues

• Clean up Cubical.Categories.Yoneda

  refactor
  agda/cubical#1285 · Filter by author maxsnew opened on Jan 6, 2026
  2

• Refactor modules for better compatibility with Cubical without Glue

  agda/cubical#1282 · Filter by author yeejian-tan opened on Dec 18, 2025
  1

• Rewrite category theory code to separate structure and properties

  agda/cubical#1267 · Filter by author mortberg opened on Oct 23, 2025
  6

• Merge Fin.Data and Fin.Data.Inductive

  good first issuerefactor
  agda/cubical#1264 · Filter by author mortberg opened on Oct 16, 2025
  1

• Define based identity systems

  agda/cubical#1254 · Filter by author anshwad10 opened on Aug 22, 2025
  1

• Redundancy between Displayed.Constructions.PropertyOver and Category.Constructions.FullSubcategory

  agda/cubical#1248 · Filter by author maxsnew opened on Aug 12, 2025
  6

• The powerset is not universe polymorphic enough

  agda/cubical#1236 · Filter by author anshwad10 opened on Jul 26, 2025
  4

• Formalize 'Combinatorics of higher-categorical diagrams' by Amar Hadzihasanovic

  agda/cubical#1218 · Filter by author anshwad10 opened on Jun 23, 2025

• Define ends and coends

  agda/cubical#1197 · Filter by author anshwad10 opened on Feb 24, 2025

• Notice: (Future) improvement to Glue usability

  discuss
  agda/cubical#1190 · Filter by author plt-amy opened on Feb 18, 2025
  3

• Move Cubical.Algebra.SymmetricGroup to Cubical.Algebra.Group.Instances.Symmetric

  agda/cubical#1186 · Filter by author anshwad10 opened on Feb 14, 2025

• Formalize Ordered CommRings

  agda/cubical#1181 · Filter by author anshwad10 opened on Jan 15, 2025

• Formalizing Devalapurkar & Haine

  agda/cubical#1147 · Filter by author Trebor-Huang opened on Aug 10, 2024

• arithmetic operations of Cubical.Data.Rationals is super slow

  agda/cubical#1124 · Filter by author onestruggler opened on Apr 29, 2024
  1

• Solver for wild categories

  agda/cubical#1118 · Filter by author felixwellen opened on Mar 24, 2024

• Make the CommRingSolver work better with concrete rings

  agda/cubical#1101 · Filter by author felixwellen opened on Feb 7, 2024

• SumMap in Algebra.Ring.BigOps should come from Semirings /Monoids

  agda/cubical#1088 · Filter by author mzeuner opened on Jan 16, 2024
  2

• Suggested heap size for CI

  agda/cubical#1074 · Filter by author felixwellen opened on Oct 30, 2023
  1

• Additions to the powerset module

  agda/cubical#1052 · Filter by author rahulc29 opened on Sep 14, 2023
  3

• Duplication of code in the library

  agda/cubical#1017 · Filter by author jpoiret opened on Jun 28, 2023
  5

• Where should π₁(RP²) be?

  question
  agda/cubical#1016 · Filter by author ice1000 opened on Jun 25, 2023
  1

• Suggestion: provide proof that set-coequalizers of finite sets are finite?

  agda/cubical#1004 · Filter by author finegeometer opened on May 7, 2023
  2

• RecordEquiv reflection doesn't seem to handle implicit field arguments

  agda/cubical#995 · Filter by author Trebor-Huang opened on Mar 8, 2023
  6

  

• Code for Data.Fin.Properties needs to migrate to Cubical.Nat.Properties/Order

  agda/cubical#978 · Filter by author xekoukou opened on Feb 1, 2023

• Consider caching Nix artifacts via Cachix

  agda/cubical#960 · Filter by author phijor opened on Nov 24, 2022