Skip to content

Issues: agda/agda-categories

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
51 Open 105 Closed
51 Open 105 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
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Compiling Categories.Category.Cartesian is very slow
#215 opened Oct 28, 2020 by jwiegley
38
Rename record fields for functorial actions and components of natural transformations
#103 opened Jan 5, 2020 by sstucki
12
Monoidal Groupoid
#106 opened Jan 6, 2020 by JacquesCarette
@JacquesCarette
5
consider adding a symmetric version of enriched category thoery
#120 opened Feb 14, 2020 by HuStmpHrrr
13
Mechanize closed/cartesian-closed enriched categories.
#121 opened Feb 15, 2020 by sstucki
Ordered families of equivalences
#127 opened Feb 28, 2020 by ajrouvoet
2
Many structures in Diagram are (co)limits enhancement New feature or request good first issue Good for newcomers help wanted Extra attention is needed
#129 opened Mar 5, 2020 by HuStmpHrrr 0.2
2
add documentation to the code documentation Improvements or additions to documentation good first issue Good for newcomers help wanted Extra attention is needed
#134 opened Mar 7, 2020 by HuStmpHrrr
8
Do we have unpacked eliminators in this library?
#142 opened Mar 19, 2020 by JacquesCarette
2
properties of presheaves
#148 opened Mar 24, 2020 by HuStmpHrrr
3
1
Topos theory
#155 opened Mar 31, 2020 by HuStmpHrrr
1
flip the equalities of Equalizer and Coequalizer to the other direction
#159 opened Apr 2, 2020 by HuStmpHrrr
Challenge: prove that the Discrete functor is the (cartesian) left-adjoint of the forgetful functor from Cats to Sets
#41 opened Aug 27, 2019 by sstucki
8
Various algebraic categories
#212 opened Oct 8, 2020 by conal
19
More general preservation of limits
#237 opened Jan 1, 2021 by JacquesCarette
Pretopos
#238 opened Jan 2, 2021 by JacquesCarette
5
Create a Proper table of contents documentation Improvements or additions to documentation help wanted Extra attention is needed
#245 opened Feb 9, 2021 by JacquesCarette
It would be nice for (1 -> C ᵒᵖ) to be the same as (1 -> C) ᵒᵖ
#256 opened Mar 3, 2021 by JasonGross
16
It would be nice to prove that Kan Extensions involving the terminal category align with (co)limits
#257 opened Mar 3, 2021 by JasonGross
1
Update definition of morphism equality in Setoids
#265 opened Apr 9, 2021 by TOTBWF
20
Exact Completion low-hanging-fruit Straightforward thing to implement
#281 opened May 26, 2021 by JacquesCarette
Is Setoids its own exact completion?
#282 opened May 26, 2021 by JacquesCarette
Rename Sets to Types ? design meta meta issue question Further information is requested
#286 opened Jun 18, 2021 by JacquesCarette
5
Multicategory of commutative monoids
#291 opened Jul 2, 2021 by laMudri
@JacquesCarette
Isbell duality is missing
#441 opened Nov 15, 2024 by tetrapharmakon
6
ProTip! Find all open issues with in progress development work with linked:pr.