Search results

Clean up Cubical.Categories.Yoneda

refactorRefactorings, e.g. renaming, moving, rearranging...Refactorings, e.g. renaming, moving, rearranging...

Status: Open.

#1285 In agda/cubical;

· maxsnew opened on Jan 6, 2026

Refactor modules for better compatibility with Cubical without Glue

Status: Open.

#1282 In agda/cubical;

· yeejian-tan opened on Dec 18, 2025

Rewrite category theory code to separate structure and properties

Status: Open.

#1267 In agda/cubical;

· mortberg opened on Oct 23, 2025

Merge Fin.Data and Fin.Data.Inductive

good first issueGood for newcomersGood for newcomers

refactorRefactorings, e.g. renaming, moving, rearranging...Refactorings, e.g. renaming, moving, rearranging...

Status: Open.

#1264 In agda/cubical;

· mortberg opened on Oct 16, 2025

Define based identity systems

Status: Open.

#1254 In agda/cubical;

· anshwad10 opened on Aug 22, 2025

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

Status: Open.

#1248 In agda/cubical;

· maxsnew opened on Aug 12, 2025

The powerset is not universe polymorphic enough

Status: Open.

#1236 In agda/cubical;

· anshwad10 opened on Jul 26, 2025

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

Status: Open.

#1218 In agda/cubical;

· anshwad10 opened on Jun 23, 2025

Define ends and coends

Status: Open.

#1197 In agda/cubical;

· anshwad10 opened on Feb 24, 2025

Notice: (Future) improvement to Glue usability

discussShould be discussed and possibly assigned in the next meetingShould be discussed and possibly assigned in the next meeting

Status: Open.

#1190 In agda/cubical;

· plt-amy opened on Feb 18, 2025

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

Status: Open.

#1186 In agda/cubical;

· anshwad10 opened on Feb 14, 2025

Formalize Ordered CommRings

Status: Open.

#1181 In agda/cubical;

· anshwad10 opened on Jan 15, 2025