Search results

Simple Bool-contradiction lemma?

addition

discoverabilityHow easy/hard will it be for users to find, within the context of their application?How easy/hard will it be for users to find, within the context of their application?

naming

Status: Open.

#2847 In agda/agda-stdlib;

· andreasabel opened on Oct 28, 2025

Use consistent names for <code>Decidable</code> combinators (#2842 redux)

Status: Open.

#2846 In agda/agda-stdlib;

· jamesmckinna opened on Oct 28, 2025

What name should we use for (instances of) <code>DecidableEquality</code>?

library-design

naming

style-guide

Status: Open.

#2845 In agda/agda-stdlib;

· jamesmckinna opened on Oct 26, 2025

Missing group isomorphism bundle and alike for other structures

Status: Open.

#2839 In agda/agda-stdlib;

· onestruggler opened on Oct 13, 2025

[ design ] use higher-level programming abstractions

library-design

Status: Open.

#2834 In agda/agda-stdlib;

· jamesmckinna opened on Sep 29, 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-compatibletries to supersede `without-K`, at a costtries to supersede `without-K`, at a cost

discussion

Status: Open.

#2792 In agda/agda-stdlib;

· JacquesCarette opened on Jul 29, 2025