-
Notifications
You must be signed in to change notification settings - Fork 73
Pull requests: UniMath/agda-unimath
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
Break the Dedekind reals into lower and upper Dedekind reals
#1314
opened Feb 10, 2025 by
lowasser
Loading…
Closure properties of π-finite types
univalent-combinatorics
#1311
opened Feb 9, 2025 by
fredrik-bakke
Loading…
Do syntax for elim-exists chains, including application to strict real inequality
experiment
#1306
opened Feb 9, 2025 by
lowasser
Loading…
Logic, equality, and compactness
foundation
logic
order-theory
set-theory
#1264
opened Feb 4, 2025 by
fredrik-bakke
•
Draft
Wild ω-semicategories
globular-types
wild-category-theory
#1229
opened Dec 1, 2024 by
fredrik-bakke
•
Draft
Refactor elementary number theory
100-theorems
elementary-number-theory
oeis
refactoring
#1211
opened Oct 25, 2024 by
EgbertRijke
•
Draft
A constructive Cantor–Schröder–Bernstein theorem
experiment
foundation
logic
order-theory
#1206
opened Oct 20, 2024 by
fredrik-bakke
•
Draft
Cleanup of @spcfox's modal logic pull request
logic
#1170
opened Aug 27, 2024 by
EgbertRijke
•
Draft
Descent and induction principle of identity types of coequalizers
enhancement
New feature or request
synthetic-homotopy-theory
#1140
opened May 18, 2024 by
VojtechStep
•
Draft
Simplicial Type Theory
do not merge
simplicial-type-theory
#1118
opened Apr 18, 2024 by
fredrik-bakke
•
Draft
Refactor graphs with updates from Beyond finite sets
graph-theory
refactoring
#879
opened Oct 22, 2023 by
EgbertRijke
•
Draft
Cleaning up for homotopy groups
group-theory
higher-group-theory
synthetic-homotopy-theory
#836
opened Oct 13, 2023 by
EgbertRijke
•
Draft
Beyond finite sets
category-theory
cleanup
graph-theory
group-theory
refactoring
trees
univalent-combinatorics
#623
opened May 15, 2023 by
EgbertRijke
•
Draft
ProTip!
Follow long discussions with comments:>50.