issues
search
plt-amy
/
1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
https://1lab.dev
GNU Affero General Public License v3.0
318
stars
61
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
chore: bump agda
#409
plt-amy
closed
8 hours ago
2
Refactor `Const`
#408
TOTBWF
closed
6 hours ago
2
Another irrelevant instance search bug
#407
ncfavier
opened
3 days ago
1
misc improvements
#406
ncfavier
closed
7 hours ago
2
Can't eliminate truncation inside `absurd`
#405
ncfavier
closed
3 days ago
3
Show statement of surjection→is-quotient
#404
plt-amy
closed
1 week ago
1
Kleisli Categories, Kleisli maps
#403
TOTBWF
closed
2 weeks ago
2
chore: add page for tracking Borceux progress
#402
TOTBWF
opened
2 weeks ago
1
FinSets is finitely (co)complete
#401
ncfavier
closed
2 weeks ago
1
container for building the 1lab
#400
4e554c4c
opened
2 weeks ago
0
Universal colimits
#399
ncfavier
closed
3 weeks ago
2
defn: equivalences over
#398
ncfavier
closed
3 weeks ago
1
web: add CSS rule for macro names
#397
ncfavier
closed
3 weeks ago
1
web: don't justify the TOC
#396
ncfavier
closed
3 weeks ago
1
chore: fix typo in Free objects
#395
szumixie
closed
4 weeks ago
1
def: injections from fibre posets to the total space
#394
favonia
closed
4 weeks ago
1
def: lexical sum of posets
#393
favonia
closed
3 weeks ago
5
Fix typo
#392
mietek
closed
1 month ago
0
def: fibre posets
#391
favonia
closed
1 month ago
1
chore: simplify code using prop-ext!
#390
favonia
closed
1 month ago
2
chore: typo
#389
ncfavier
closed
1 month ago
1
chore: add Funlike instance for Total-hom
#388
favonia
closed
1 month ago
1
chore: use "Id", not "id", for identity functor
#387
favonia
closed
1 month ago
1
chore: fix grammar
#386
ncfavier
closed
1 month ago
2
Fix typos
#385
juanmeleiro
closed
1 month ago
1
chore: fix typos in Cat.Bi.Diagram.Monad
#384
favonia
closed
1 month ago
1
very minor grammar issue
#383
vcvpaiva
closed
1 month ago
0
CITATION: bump year, fix author
#382
ncfavier
closed
1 month ago
1
def: 1-category Monad(C)
#381
favonia
closed
1 month ago
4
chore: fix typo
#380
favonia
closed
1 month ago
1
wording: dust off 1Lab.Path
#379
plt-amy
closed
1 month ago
1
defn: lifting for posets and monotone maps
#378
favonia
closed
1 month ago
2
chore: Fix typo
#377
FernandoChu
closed
2 months ago
3
def: macros for creating copattern definitions
#376
TOTBWF
closed
3 weeks ago
6
Simplex Category
#375
TOTBWF
opened
3 months ago
2
chore: add hlevel instance for singletons, simplify `prop!`
#374
ncfavier
closed
8 hours ago
1
defn: generic elim!/rec!
#373
plt-amy
closed
3 months ago
1
equivalence implies identity system
#372
ncfavier
closed
3 months ago
13
chore: bump agda
#371
plt-amy
closed
3 months ago
1
chore: bump actions
#370
ncfavier
closed
3 months ago
1
Sites and sheaves
#369
plt-amy
closed
3 weeks ago
3
chore: bump agda
#368
plt-amy
closed
4 months ago
0
chore: misc fixes
#367
ncfavier
closed
4 months ago
1
Strong, commutative, idempotent, monoidal monads
#366
ncfavier
closed
4 months ago
1
Fix a typo: swap g & h; Add diagrams
#365
cxandru
closed
4 months ago
2
Basic monoidal category theory
#364
ncfavier
closed
4 months ago
1
No spacing between heading and code block
#363
ncfavier
closed
3 weeks ago
2
chore: re-write 1Lab.HLevel
#362
plt-amy
closed
4 months ago
1
Cleanup, rewrite 1Lab.Equiv, the opposite of a fibration
#361
plt-amy
closed
4 months ago
1
chore: bump agda
#359
plt-amy
closed
5 months ago
1
Next