issues
search
agda
/
agda-categories
A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
359
stars
67
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Caching on CI seems to be broken
#375
JacquesCarette
closed
9 months ago
12
added unique choice
#374
sergey-goncharov
closed
1 year ago
0
the naturality conditions for ann and distrib were missing.
#373
JacquesCarette
closed
1 year ago
1
Bump Agda to 2.6.3 and stdlib to 1.7.2
#372
jpoiret
closed
1 year ago
3
ramp up stdlib version?
#371
HuStmpHrrr
opened
1 year ago
14
WIP: right adjoint to Functor.Slice.Free
#370
Taneb
closed
6 months ago
4
Fix typos in comments
#369
epost
closed
1 year ago
1
Fix typo 'mupliple' -> 'multiple'
#368
epost
closed
1 year ago
0
Add right adjoint to Functor.Slice.Forgetful
#367
Taneb
closed
1 year ago
2
`!-unique₂` takes implicit args in `Terminal`, whereas it takes explicit ones in `Initial`
#366
cxandru
opened
1 year ago
1
Make Rels less strict, add a StrictRels for the previous version
#365
Taneb
opened
1 year ago
3
Add uncurry and composition with curry
#364
iwilare
closed
1 year ago
0
Remove Categories.Category.Equivalence
#363
iwilare
opened
1 year ago
1
μ-Bialgebras
#362
cxandru
closed
1 year ago
7
Prove that Nat is cartesian and Natop is hence cocartesian
#361
Taneb
closed
1 year ago
0
Parametric adjunctions form cowedges
#360
iwilare
closed
1 year ago
0
Add `IsNI` to be consistent with `IsIso` in for morphisms
#359
91khr
closed
1 year ago
0
Add the category of predicates over agda types
#358
cmcmA20
closed
1 year ago
1
Move Categories.Category.Diagram.Span to Categories.Diagram.Span
#357
Taneb
opened
1 year ago
0
Rels is also a symmetric monoidal category with Set's cartesian product
#356
Taneb
closed
1 year ago
1
Simplex: degen is pinch from agda-stdlib
#355
phadej
closed
1 year ago
1
F-Coalgebras form a category
#354
Taneb
closed
1 year ago
3
Pull out adjunction between products and exponentials
#353
HuStmpHrrr
opened
1 year ago
1
make it work with the agda stdlib v2.0 (c12568c64)
#352
cmcmA20
closed
6 months ago
11
Maybe the Hom version of Adjunction can be fully polymorphic?
#351
JacquesCarette
opened
2 years ago
1
Removing a redundant field in CartesianClosed/Canonical
#350
MiddleAdjunction
closed
2 years ago
1
[draft] Add definition of an adjunction in Bicategory
#348
Boarders
opened
2 years ago
4
Cleaning up Slice Functor and surrounding infrastructure
#347
JacquesCarette
closed
6 months ago
7
[draft] Add draft definition of a double category
#346
Boarders
closed
1 year ago
7
2-Terminal Object and 2-Product
#345
maxsnew
closed
2 years ago
4
Naming of fields in CartesianClosed Functor
#344
JacquesCarette
opened
2 years ago
2
bicategory renaming
#343
maxsnew
closed
2 years ago
0
Move Everything.agda to src.
#342
anuyts
closed
2 years ago
10
Field names for RegularEpi/RegularMono are nondescriptive
#341
TOTBWF
opened
2 years ago
6
Extremal Morphisms
#340
TOTBWF
closed
2 years ago
2
Add bundled CCCs and basic def. for CC functors.
#339
Trebor-Huang
closed
2 years ago
3
Bicategory terminology
#338
maxsnew
closed
2 years ago
4
Implementation of Lax Slice bicategory
#337
maxsnew
closed
2 years ago
3
Prove that Cats is complete
#336
Taneb
closed
5 months ago
9
Exact
#335
sergey-goncharov
closed
2 years ago
0
Suggested improvements for `IsPullback`
#334
JacquesCarette
opened
2 years ago
1
Define Lifting Properties
#333
TOTBWF
closed
2 years ago
3
Spelling mistake in Categories.Morphism.HeterogeneousIdentity
#332
Icelandjack
closed
2 years ago
1
Group objects
#331
Taneb
closed
2 years ago
0
Discrepancy of `unique` of `Product` and `unique` of `IsPullback`
#329
sergey-goncharov
opened
2 years ago
1
Internal Relations and Exactness
#328
sergey-goncharov
closed
2 years ago
0
Alternate version of Setoids being Extensive
#327
JacquesCarette
closed
2 years ago
0
Create Adjunctions.agda
#326
tetrapharmakon
opened
2 years ago
3
Free objects construction update
#325
yourboynico
closed
2 years ago
0
Update Kleisli.agda
#324
tetrapharmakon
closed
2 years ago
1
Previous
Next