Search results

Define based identity systems

Status: Open.

#1254 In agda/cubical;

· anshwad10 opened on Aug 22, 2025

Inconsistency between Iso and Category.isIso

good first issueGood for newcomersGood for newcomers

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

Status: Open.

#1251 In agda/cubical;

· maxsnew opened on Aug 20, 2025

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

Status: Open.

#1248 In agda/cubical;

· maxsnew opened on Aug 12, 2025

Category and Displayed Category Performance aka Should we no-eta-equality Category?

Status: Open.

#1240 In agda/cubical;

· maxsnew opened on Jul 29, 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 <code>Cubical.Algebra.SymmetricGroup</code> to <code>Cubical.Algebra.Group.Instances.Symmetric</code>

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

Formalizing Devalapurkar &amp; Haine

Status: Open.

#1147 In agda/cubical;

· Trebor-Huang opened on Aug 10, 2024

arithmetic operations of Cubical.Data.Rationals is super slow

Status: Open.

#1124 In agda/cubical;

· onestruggler opened on Apr 29, 2024