issues
search
the1lab
/
1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
https://1lab.dev
GNU Affero General Public License v3.0
333
stars
63
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Solver for equations over ℚ
#431
plt-amy
opened
1 day ago
1
chore: bump agda
#430
plt-amy
closed
1 day ago
1
ring localisations and rational numbers
#429
plt-amy
closed
4 days ago
1
Yet another irrelevant instance bug
#428
ncfavier
opened
2 weeks ago
0
Basic group theory
#427
ncfavier
closed
1 week ago
1
Enable search on mobile
#426
hmltn-0
opened
2 weeks ago
0
fixup type hover
#425
plt-amy
closed
2 weeks ago
1
Point-set topology
#424
TOTBWF
opened
1 month ago
0
Flat records for (co)cartesian fibrations.
#423
TOTBWF
opened
1 month ago
0
Free categories, categories from generators and relations
#422
TOTBWF
opened
1 month ago
1
Set-projective types and projective objects
#421
TOTBWF
closed
1 month ago
1
Projective Objects
#420
TOTBWF
closed
1 month ago
0
chore: misc nonsense
#419
ncfavier
closed
1 month ago
1
Added (homotopy) Pushouts and Cocones, and some features/examples of said.
#418
jake-87
opened
1 month ago
3
Flat records for limits/colimits
#417
TOTBWF
opened
1 month ago
4
wip: prime numbers
#416
plt-amy
closed
1 month ago
1
Biproducts and semiadditive categories
#415
ncfavier
closed
1 month ago
1
Flat records for (co)limits
#414
TOTBWF
opened
1 month ago
0
Separating objects
#413
TOTBWF
closed
1 month ago
3
Separating Objects
#412
TOTBWF
closed
1 month ago
0
wip: elementary topos nonsense
#411
plt-amy
opened
1 month ago
2
Low hanging fruit regarding limits
#410
TOTBWF
closed
1 month ago
1
chore: bump agda
#409
plt-amy
closed
1 month ago
2
Refactor `Const`
#408
TOTBWF
closed
1 month ago
2
Another irrelevant instance search bug
#407
ncfavier
opened
2 months ago
1
misc improvements
#406
ncfavier
closed
1 month ago
2
Can't eliminate truncation inside `absurd`
#405
ncfavier
closed
2 months ago
3
Show statement of surjection→is-quotient
#404
plt-amy
closed
2 months ago
1
Kleisli Categories, Kleisli maps
#403
TOTBWF
closed
2 months ago
2
chore: add page for tracking Borceux progress
#402
TOTBWF
closed
1 month ago
2
FinSets is finitely (co)complete
#401
ncfavier
closed
2 months ago
1
container for building the 1lab
#400
4e554c4c
opened
2 months ago
0
Universal colimits
#399
ncfavier
closed
2 months ago
2
defn: equivalences over
#398
ncfavier
closed
2 months ago
1
web: add CSS rule for macro names
#397
ncfavier
closed
2 months ago
1
web: don't justify the TOC
#396
ncfavier
closed
2 months ago
1
chore: fix typo in Free objects
#395
szumixie
closed
2 months ago
1
def: injections from fibre posets to the total space
#394
favonia
closed
2 months ago
1
def: lexical sum of posets
#393
favonia
closed
2 months ago
5
Fix typo
#392
mietek
closed
3 months ago
0
def: fibre posets
#391
favonia
closed
3 months ago
1
chore: simplify code using prop-ext!
#390
favonia
closed
3 months ago
2
chore: typo
#389
ncfavier
closed
3 months ago
1
chore: add Funlike instance for Total-hom
#388
favonia
closed
3 months ago
1
chore: use "Id", not "id", for identity functor
#387
favonia
closed
3 months ago
1
chore: fix grammar
#386
ncfavier
closed
3 months ago
2
Fix typos
#385
juanmeleiro
closed
3 months ago
1
chore: fix typos in Cat.Bi.Diagram.Monad
#384
favonia
closed
3 months ago
1
very minor grammar issue
#383
vcvpaiva
closed
3 months ago
0
CITATION: bump year, fix author
#382
ncfavier
closed
3 months ago
1
Next