Skip to content

Pull requests: UniMath/agda-unimath

New pull request New
47 Open 1,184 Closed
47 Open 1,184 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Fix name type sequences posets
#1407 opened Apr 22, 2025 by malarbol Loading…
Arithmetic-geometric mean inequality on the rational numbers elementary-number-theory
#1406 opened Apr 18, 2025 by lowasser Loading…
22
Reframe limited principle of omniscience and variants in terms of decidable subtypes foundation
#1404 opened Apr 11, 2025 by lowasser Loading…
18
total metric spaces
#1403 opened Apr 11, 2025 by malarbol • Draft
2
Short limit map convergent Cauchy approximations
#1402 opened Apr 10, 2025 by malarbol • Draft
2
sequences large preorders/posets
#1399 opened Apr 7, 2025 by malarbol • Draft
2
Real functions
#1398 opened Apr 7, 2025 by malarbol • Draft
7
Refactor linear algebra to use "tuples" for what was "vectors" improve naming linear-algebra refactoring
#1397 opened Apr 6, 2025 by lowasser Loading…
3
Linear maps over modules group-theory linear-algebra ring-theory
#1395 opened Apr 3, 2025 by lowasser Loading…
15
Distance function on real numbers metric-spaces order-theory real-numbers
#1394 opened Apr 3, 2025 by lowasser Loading…
12
simplicial type theory
#1393 opened Apr 2, 2025 by EgbertRijke • Draft
More logic foundation logic
#1387 opened Mar 28, 2025 by fredrik-bakke Loading…
45
Multiplication of real numbers real-numbers
#1384 opened Mar 26, 2025 by lowasser • Draft
1
Coherently constant maps foundation
#1383 opened Mar 26, 2025 by fredrik-bakke Loading…
Preview: depostulate axioms do not merge experiment
#1380 opened Mar 24, 2025 by fredrik-bakke Loading…
3
Limits of sequences in metric spaces elementary-number-theory foundation metric-spaces
#1378 opened Mar 24, 2025 by malarbol • Draft
36
Level-polymorphic commutative monoid of lower and upper Dedekind real numbers under addition real-numbers
#1377 opened Mar 23, 2025 by lowasser • Draft
1
Equivalence between a type and the coproduct of a decidable subtype and its complement foundation logic
#1376 opened Mar 23, 2025 by lowasser • Draft
11
Commutative semiring of formal power series on commutative semirings commutative-algebra
#1374 opened Mar 21, 2025 by lowasser • Draft
2
Remove dependency between BUILTIN and postulates elementary-number-theory experiment foundation refactoring reflection
#1373 opened Mar 20, 2025 by fredrik-bakke Loading…
3
Bernoulli's inequality on the positive rational numbers elementary-number-theory
#1371 opened Mar 19, 2025 by malarbol Loading…
75
Zigzag construction of identity types of pushouts enhancement New feature or request 🏆 milestone 🏆 synthetic-homotopy-theory
#1370 opened Mar 18, 2025 by VojtechStep • Draft
1 of 5 tasks
6
Streams lists
#1368 opened Mar 17, 2025 by djspacewhale • Draft
1
Sums and products over arbitrary finite types commutative-algebra finite-group-theory group-theory linear-algebra ring-theory univalent-combinatorics
#1367 opened Mar 16, 2025 by lowasser Loading…
89
Flattening lemma for equifibered dependent span diagrams synthetic-homotopy-theory
#1366 opened Mar 15, 2025 by fredrik-bakke • Draft
2 of 4 tasks
ProTip! Adding no:label will show everything without a label.