Search results

Definition of cotransitivty is wrong

bugSomething isn't workingSomething isn't working

foundation

order-theory

Status: Open.

#1803 In UniMath/agda-unimath;

· fredrik-bakke opened on Jan 30, 2026

Rationalize interval terminology

improve naming

Status: Open.

#1800 In UniMath/agda-unimath;

· lowasser opened on Jan 27, 2026

Free algebraic constructions

trees

universal-algebra

Status: Open.

#1797 In UniMath/agda-unimath;

· lowasser opened on Jan 18, 2026

Consider rebuilding the concept of matrix around finite sequences instead of tuples

linear-algebra

refactoring

Status: Open.

#1791 In UniMath/agda-unimath;

· lowasser opened on Jan 8, 2026

The Banach-Tarski paradox

Wikipedia theorems

Status: Open.

#1790 In UniMath/agda-unimath;

· lowasser opened on Jan 8, 2026

Generalize invertible real functions

real-numbers

Status: Open.

#1759 In UniMath/agda-unimath;

· lowasser opened on Dec 22, 2025

Rename <code>Rational-Extension-Ring</code> to <code>ℚ-Extension-Ring</code>

elementary-number-theory

improve naming

ring-theory

Status: Open.

#1725 In UniMath/agda-unimath;

· fredrik-bakke opened on Nov 23, 2025

Consider an alternate definition of continuity

analysis

improve naming

metric-spaces

Status: Open.

#1715 In UniMath/agda-unimath;

· lowasser opened on Nov 15, 2025

Naming of reflective global subuniverses

improve naming

orthogonal-factorization-systems

questionFurther information is requestedFurther information is requested

Status: Open.

#1711 In UniMath/agda-unimath;

· fredrik-bakke opened on Nov 14, 2025

L'Hôpital's Rule

100 theorems

analysis

Status: Open.

#1701 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Non-denumerability of the continuum

100 theorems

real-numbers

Status: Open.

#1699 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025

Riemann integration

analysis

Status: Open.

#1698 In UniMath/agda-unimath;

· lowasser opened on Nov 11, 2025