Search results

[ design ] use higher-level programming abstractions

library-design

Status: Open.

#2834 In agda/agda-stdlib;

· jamesmckinna opened on Sep 29, 2025

<code>¬∃⇒∀¬</code>

Status: Open.

#2831 In agda/agda-stdlib;

· mechvel opened on Sep 25, 2025

Prove that Permutation' n is isomorphic to Fin (n !)

Status: Open.

#2827 In agda/agda-stdlib;

· Taneb opened on Sep 10, 2025

[ add ] <code>Setoid</code>/<code>IsEquivalence</code> bundle/structure of propositions modulo bi-implication

addition

Status: Open.

#2820 In agda/agda-stdlib;

· jamesmckinna opened on Aug 29, 2025

<code>Factorization</code> and <code>factor</code>

Status: Open.

#2818 In agda/agda-stdlib;

· mechvel opened on Aug 28, 2025

[ add ] Upwards- and downwards- closed subsets of a given ordered set

addition

subsetsrelies on/infleunced by/influences, various approaches to the notion of 'subset(oid)' in type theoryrelies on/infleunced by/influences, various approaches to the notion of 'subset(oid)' in type theory

Status: Open.

#2814 In agda/agda-stdlib;

· jamesmckinna opened on Aug 21, 2025

Orientation of the equation <code>Algebra.Properties.RingWithoutOne.-‿distribˡ-*</code>

Status: Open.

#2807 In agda/agda-stdlib;

· jamesmckinna opened on Aug 12, 2025

[ design ] Re-exports from <code>Algebra.Properties.X</code>

breaking

dependencies

documentation

library-design

Status: Open.

#2804 In agda/agda-stdlib;

· jamesmckinna opened on Aug 4, 2025

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: Open.

#2786 In agda/agda-stdlib;

· jamesmckinna opened on Jul 27, 2025

· 

v2.4

Suggestion for List/Over folders.

Status: Open.

#2780 In agda/agda-stdlib;

· mechvel opened on Jul 19, 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