issues
search
jonsterling
/
coq-domains
http://www.jonmsterling.com/coq-domains/toc.html
18
stars
1
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Eventually switch to using surjectivity from mathcomp?
#30
clayrat
opened
2 years ago
0
Preorder skeleton and intuitionistic well-founded preorders
#29
jonsterling
closed
2 years ago
0
Make Lift be Dcpo -> Dcppo rather than Type -> Dcppo
#28
jonsterling
closed
2 years ago
0
Definition of the lift is wrong LOL
#27
jonsterling
closed
2 years ago
0
Working on filtered bilimits in dcpo
#26
jonsterling
opened
2 years ago
0
Develop lifting *comonad* on Eilenberg-Mac Lane category
#25
jonsterling
opened
2 years ago
0
Kleisli category of the lift monad
#24
jonsterling
opened
2 years ago
0
Construction of filtered bilimits in Dcpo
#23
jonsterling
opened
2 years ago
0
Formal \omega-cpos
#22
jonsterling
opened
2 years ago
0
Admissibility stuff
#21
jonsterling
opened
2 years ago
0
Prove fixed point induction for admissible predicates
#20
jonsterling
closed
2 years ago
1
fixed point induction
#19
jonsterling
closed
2 years ago
0
Define the upper naturals
#18
jonsterling
closed
2 years ago
2
Add ideal completions?
#17
clayrat
opened
3 years ago
1
lift monadicity
#16
clayrat
closed
3 years ago
0
Refactor a bit
#15
clayrat
closed
3 years ago
0
Universal property of Lift
#14
jonsterling
closed
3 years ago
2
universal property of lift
#13
jonsterling
closed
3 years ago
0
unify definitions of continuity, move to poset
#12
jonsterling
closed
3 years ago
0
tweaks
#11
clayrat
closed
3 years ago
0
Stupid elpi warnings
#10
jonsterling
opened
3 years ago
0
Unify equivalent definitions of continuity
#9
jonsterling
closed
3 years ago
0
add Kleene's LFP theorem
#8
clayrat
closed
3 years ago
0
Publish github pages without checking the html into git
#6
jonsterling
closed
3 years ago
8
Somewhat more idiomatic SSReflect
#5
clayrat
closed
3 years ago
11
formalize Sierpinski path relation
#4
jonsterling
closed
3 years ago
0
define lift à la de Jong / Escardó
#3
jonsterling
closed
3 years ago
0
prove universal property of dcpo exponential
#2
jonsterling
opened
3 years ago
0
add cartesian product of dcpos
#1
jonsterling
closed
3 years ago
0