Skip to content

Pull requests: agda/cubical

New pull request New
24 Open 178 Closed
24 Open 178 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
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Category/Presheaf notations, univalent displayed categories, Displayed categories in BinProduct and Elements
#1305 opened Apr 23, 2026 by maxsnew Collaborator Loading…
core code missing from Nat and Int
#1304 opened Apr 23, 2026 by reswatson Contributor Loading…
2
Properties of OrderedCommRings
#1303 opened Apr 21, 2026 by LorenzoMolena Contributor Loading…
Add Iterative Sets
#1300 opened Mar 24, 2026 by flgrubm Contributor • Draft
51
BooleanAlgebraStr now infers the underlying set
#1297 opened Mar 3, 2026 by Freek98 Contributor Loading…
2
Comm ring solver improvement
#1293 opened Feb 17, 2026 by marcinjangrzybowski Contributor • Draft
4
Define multicategories
#1278 opened Nov 24, 2025 by anshwad10 Contributor • Draft
Heap
#1277 opened Nov 22, 2025 by anshwad10 Contributor Loading…
Enriched Orders
#1255 opened Aug 27, 2025 by anshwad10 Contributor • Draft
New notion of equivalence: Bijective relations
#1252 opened Aug 20, 2025 by anshwad10 Contributor Loading…
14
Improvements to Univalence.agda
#1237 opened Jul 27, 2025 by anshwad10 Contributor • Draft
7
Prime (and composite) numbers
#1228 opened Jul 16, 2025 by qlbrpl Loading…
@felixwellen
19
Antithesis translation and double-negation translation
#1216 opened Jun 18, 2025 by anshwad10 Contributor • Draft
Distributive Laws of Monadic Containers
#1213 opened Jun 5, 2025 by stefaniatadama Contributor • Draft
Make join-assoc level-polymorphic
#1204 opened May 5, 2025 by ricky136973 Loading…
5
Some properties of connected spaces
#1202 opened Mar 7, 2025 by phijor Contributor Loading…
5
X is a regular element in the HIT-based polynomials
#927 opened Sep 12, 2022 by felixwellen Collaborator • Draft
Base change of algebras is functorial
#926 opened Sep 12, 2022 by felixwellen Collaborator • Draft
2LTT, External Cubes and Cube Filling Macros
#910 opened Aug 23, 2022 by kangxyz Contributor • Draft
19
Added Dependent N-Ary Vector
#908 opened Aug 23, 2022 by guilhermehas Contributor • Draft
Cubical subtyping demo: get rid of inS/outS agda Agda implementation issues refactor Refactorings, e.g. renaming, moving, rearranging...
#906 opened Aug 19, 2022 by plt-amy Contributor • Draft
4
Beefing up adjunctions.
#873 opened Jul 28, 2022 by anuyts Contributor • Draft
18
Datatype ~= coproduct of Σ-types via reflection
#871 opened Jul 25, 2022 by anuyts Contributor • Draft
1
Self contained version of the new Brunerie number
#853 opened Jun 30, 2022 by mortberg Collaborator • Draft
3
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.