Issues

• [ refactor ] where should (Is)SubX and how-to-construct-such from an IsXMonomorphism live?

  additionbreakinglibrary-designrefactoring
  agda/agda-stdlib#3143 · Filter by author jamesmckinna opened on Nov 13, 2026

• [ add ] (yet) more Algebra.Properties.* re-exports: (yet) more diamonds

  additiondependencieslibrary-design
  agda/agda-stdlib#3139 · Filter by author jamesmckinna opened on Nov 10, 2026
  1

• More about Data.Rational.Properties

  library-designrefactoring
  agda/agda-stdlib#3136 · Filter by author jamesmckinna opened on Nov 6, 2026
  2

• [ add ] positive rationals ℚ⁺ as a type in their own right, with... suitable Properties

  additionlibrary-design
  agda/agda-stdlib#3134 · Filter by author jamesmckinna opened on Nov 3, 2026
  5

• takeWhile-accept and others

  agda/agda-stdlib#3130 · Filter by author mechvel opened on Oct 25, 2026

• Needs lib-2.4 dropWhile⁺ in All ?

  agda/agda-stdlib#3121 · Filter by author mechvel opened on Sep 22, 2026

• [ views ] 'smart(er) constructors', 'destructor form', ... how to describe/systematise this phenomenon?

  agda/agda-stdlib#3113 · Filter by author jamesmckinna opened on Sep 4, 2026

• New branch agda-master working with the master version of Agda

  upstream
  agda/agda-stdlib#3112 · Filter by author andreasabel opened on Aug 29, 2026
  5

• [ Regex ] search with fromStart = true does not match as expect; request for documentation

  agda/agda-stdlib#3109 · Filter by author joha2 opened on Aug 22, 2026

• [ fix ] Outstanding issues with existing Tactic.*Solver and Algebra.Solver.* implementations

  Task

  agda/agda-stdlib#3105 · Filter by author jamesmckinna opened on Aug 4, 2026 · v3.0

• [ refactor ] sort out the argument + constructor names in Relation.Binary.Closure.ReflexiveTransitive

  namingrefactoring
  agda/agda-stdlib#3103 · Filter by author jamesmckinna opened on Aug 1, 2026
  1

• Items for SetoidMonomorphism

  agda/agda-stdlib#3096 · Filter by author mechvel opened on Jul 30, 2026
  1

• [ add ] 'lax squares' in Relation.Binary and their horizontal/vertical compositions

  agda/agda-stdlib#3093 · Filter by author jamesmckinna opened on Jul 28, 2026
  4

• [ refactor ] rename + deprecate Data.List.Base. _∷ʳ′_

  deprecationlibrary-designnamingrefactoring
  agda/agda-stdlib#3089 · Filter by author jamesmckinna opened on Jul 26, 2026

• Add Queue datatype

  agda/agda-stdlib#3083 · Filter by author silas-hw opened on Jul 20, 2026

• map-cong for Setoid as a co-domain?

  agda/agda-stdlib#3082 · Filter by author mechvel opened on Jul 20, 2026
  4

• Create abstraction barrier for _≤?_ from Data.Nat.Properties

  agda/agda-stdlib#3074 · Filter by author JacquesCarette opened on Jul 15, 2026
  2

• [ add ] Function.Metric.Core.DistanceRelation

  agda/agda-stdlib#3068 · Filter by author jamesmckinna opened on Jul 10, 2026

• [ refactor ] Renaming concepts in Relation.Binary.{Definitions|Structures|Bundles}

  breakingrefactoring
  agda/agda-stdlib#3058 · Filter by author jamesmckinna opened on Jul 8, 2026
  1

• [ question ] differences between Reasoning.Binary.Preorder and Reasoning.Binary.PartialOrder?

  agda/agda-stdlib#3047 · Filter by author jamesmckinna opened on Jul 2, 2026
  12

• Write a stdlib tutorial

  agda/agda-stdlib#3045 · Filter by author JacquesCarette opened on Jul 1, 2026

• [ add ] EverythingDEPRECATED?

  agda/agda-stdlib#3038 · Filter by author jamesmckinna opened on Jun 30, 2026
  4

• Add checks for defunct and orphaned READMEs to CI

  agda/agda-stdlib#3037 · Filter by author silas-hw opened on Jun 29, 2026
  2

• [ refactor ] Algebra.Morphism wrt re-exports from Algebra.Morphism.Definitions

  agda/agda-stdlib#3035 · Filter by author jamesmckinna opened on Jun 25, 2026
  4

• Deleting Function.Bijection and friends?

  deprecationlibrary-designlow-hanging-fruitrefactoring
  agda/agda-stdlib#3033 · Filter by author JacquesCarette opened on Jun 24, 2026 · v3.0
  6