issues
search
b-mehta
/
topos
Topos theory in lean
55
stars
2
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Automatic upgrade has failed
#38
github-actions[bot]
opened
3 years ago
0
Automatic upgrade has failed
#37
github-actions[bot]
closed
3 years ago
1
Automatic upgrade has failed
#36
github-actions[bot]
closed
4 years ago
1
Automatic upgrade has failed
#35
github-actions[bot]
closed
4 years ago
2
update CI
#34
robertylewis
closed
4 years ago
3
Lean 3.7.2 and new mathlib
#33
Vtec234
closed
4 years ago
6
Kleisli categories
#32
Vtec234
opened
4 years ago
0
Kleisli categories
#31
Vtec234
closed
4 years ago
3
Add uniqueness of adjoints
#30
thjread
closed
4 years ago
0
Lean 3.6.1 and new mathlib
#29
Vtec234
closed
4 years ago
0
Improve epi-mono factorisation
#28
b-mehta
opened
4 years ago
0
Creating connected limits
#27
b-mehta
closed
4 years ago
3
Pullback of isomorphism
#26
b-mehta
closed
4 years ago
0
Epi-mono factorisation in LCCC
#25
b-mehta
closed
4 years ago
0
`star f` can be identified with taking pullbacks
#24
b-mehta
closed
4 years ago
1
In an LCC, pullback preserves epi
#23
b-mehta
closed
4 years ago
0
Escaping the trunc?
#22
Vtec234
closed
4 years ago
3
Add (-)^1 = id
#21
thjread
closed
4 years ago
18
reflexive coequalizers
#20
b-mehta
opened
4 years ago
0
[meta] Projects
#19
b-mehta
closed
4 years ago
0
(-)^1 is iso to id
#18
b-mehta
closed
4 years ago
2
evaluation and coevaluation for cartesian closed cats
#17
b-mehta
closed
4 years ago
1
exponential is contrafunctorial in its other argument
#16
b-mehta
closed
4 years ago
1
`adjunction_of_nat_iso_right`
#15
b-mehta
closed
4 years ago
1
Uniqueness of adjunctions
#14
b-mehta
closed
4 years ago
4
Johnstone's exercise
#13
b-mehta
opened
4 years ago
0
Composition of monos is mono
#12
b-mehta
closed
4 years ago
0
Cone equivalences means apex equivalence
#11
b-mehta
closed
4 years ago
0
move comma.lean and pullback.lean to mathlib
#10
EdAyers
opened
4 years ago
0
Write a tactic `rewrite_assoc` that performs rewriting mod associativity of composition.
#9
EdAyers
opened
4 years ago
2
add a readme with build instructions etc
#8
EdAyers
closed
4 years ago
0
Generalise `limit.lift_self_id` etc to cones.
#7
EdAyers
opened
4 years ago
1
Merge grothendieck.lean from Ed's branch
#6
EdAyers
closed
4 years ago
1
(Type ?m) has a subobject classifier
#5
EdAyers
closed
4 years ago
2
Cartesian closed
#4
b-mehta
closed
4 years ago
3
Theorem I.5.2 (Colimit of representables)
#3
b-mehta
closed
4 years ago
1
Put a roadmap here
#2
b-mehta
closed
4 years ago
0
Add some pullback lemmas and prelims for subobject functor.
#1
EdAyers
closed
4 years ago
1