Search results

Why we should revert stdlib to <code>--without-K</code> instead of using <code>--cubical-compatible</code>

cubical-compatiblesupersedes `without-K`supersedes `without-K`

discussion

Status: Open.

#2792 In agda/agda-stdlib;

· JacquesCarette opened on Jul 29, 2025

[ deprecate ] <code>Data.Fin.Base.lower₁</code> in favour of <code>Data.Fin.Base.lower</code>

deprecation

refactoring

status: blocked-by-issueProgress on this issue or PR is blocked by another issue.Progress on this issue or PR is blocked by another issue.

Status: Open.

#2786 In agda/agda-stdlib;

· jamesmckinna opened on Jul 27, 2025

· 

v2.4

[ add ] new name for <code>flip</code>ped version of <code>Relation.Nullary.Negation.Core.contradiction</code>

library-design

Status: Open.

#2784 In agda/agda-stdlib;

· jamesmckinna opened on Jul 26, 2025

Suggestion for List/Over folders.

Status: Open.

#2780 In agda/agda-stdlib;

· mechvel opened on Jul 19, 2025

[Add] takeNat for Vec in Data.Vec.Base

Status: Open.

#2778 In agda/agda-stdlib;

· e-mniang opened on Jul 18, 2025

[ refactor ] change type of <code>Data.Vec.Base.{truncate|padRight}</code>

refactoring

Status: Open.

#2770 In agda/agda-stdlib;

· jamesmckinna opened on Jul 15, 2025

[ add ] <code>Level</code>-lifting for <code>Relation.Binary.{Structures|Bundles}</code> and <code>Algebra.{Structures|Bundles}</code>

Status: Open.

#2767 In agda/agda-stdlib;

· jamesmckinna opened on Jul 13, 2025

Setoid for List composed n-times: second level is constrained to &gt;= first level

Status: Open.

#2766 In agda/agda-stdlib;

· mechvel opened on Jul 11, 2025

[ definition ] characteristic of a <code>Ring</code> (etc.)

addition

library-design

question

Status: Open.

#2760 In agda/agda-stdlib;

· jamesmckinna opened on Jul 7, 2025

[ deprecate ] <code>Relation.Nullary.Reflects</code> and [ refactor ] <code>Relation.Nullary.Decidable.Core</code>

breaking

dependencies

deprecation

discussion

refactoring

Status: Open.

#2741 In agda/agda-stdlib;

· jamesmckinna opened on Jun 21, 2025

[ add ] lifting <code>{to|from}Witness</code> from <code>Relation.Nullary.Decidable.Core</code> to <code>Relation.Unary</code> and <code>Relation.Binary</code>

addition

refactoring

Status: Open.

#2735 In agda/agda-stdlib;

· jamesmckinna opened on Jun 18, 2025

Cantor-Schröder-Bernstein, redux

addition

refactoring

Status: Open.

#2728 In agda/agda-stdlib;

· jamesmckinna opened on Jun 5, 2025