issues
search
martinescardo
/
TypeTopology
Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220
stars
40
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Indexing Part II
#297
tomdjong
opened
2 hours ago
0
Index for "Domain Theory in UF I"
#296
tomdjong
closed
4 days ago
1
Indexing domain theory papers
#295
tomdjong
closed
4 days ago
2
A few lemmas for the formalizations of connections between small and connected types
#294
IanRay11
opened
1 week ago
0
Add prove that `ap` of an equivence is an equivalence
#293
tomdjong
closed
1 week ago
0
Ideal completion has all small joins
#292
tomdjong
closed
1 week ago
0
Show mediating map from ideal completion is unique
#291
tomdjong
closed
1 week ago
0
update line and file count
#290
martinescardo
opened
2 weeks ago
1
If the flat natural numbers are ω-complete, then LPO holds
#289
tomdjong
closed
2 weeks ago
2
Basics on omega-chains
#288
tomdjong
closed
2 weeks ago
0
Lifting in the presence of excluded middle
#287
tomdjong
closed
2 weeks ago
3
The lifting of a large proposition as an algebraic dcpo
#286
tomdjong
closed
3 weeks ago
1
A type with a nontrivial apartness relation cannot be injective unless WEM holds.
#285
tomdjong
closed
1 month ago
0
Take some first steps in the formalization of synthetic topology in UF
#284
ayberkt
opened
1 month ago
0
Lemma about simulations and initial segments of ordinals
#283
tomdjong
closed
1 month ago
0
The large dcpo of ordinals
#282
tomdjong
closed
1 month ago
1
Proof of Zorn's lemma
#281
keltono
closed
2 weeks ago
9
Third step of Stone duality for spectral locales
#280
ayberkt
opened
1 month ago
0
Prove that the sharp elements of a Scott domain coincide with the spectral points of its Scott locale
#279
ayberkt
closed
1 month ago
1
Add proof of the fact that disjunction preserves decidability
#278
ayberkt
closed
1 month ago
0
Every ordinal is the supremum of the successors of its initial segments.
#277
tomdjong
closed
1 month ago
0
Take some first steps in investigating System F resizing as an axiom
#276
ayberkt
opened
1 month ago
0
Document convention on the padding of code blocks
#275
ayberkt
closed
1 month ago
0
Do some preparation for the result on sharp elements
#274
ayberkt
closed
1 month ago
4
Fix commented code and minor issues from thesis-pr
#273
tnttodda
closed
1 month ago
1
Update `CONTRIBUTING.md`
#272
ayberkt
closed
2 months ago
0
Fix incorrect terminology
#271
ayberkt
closed
2 months ago
0
Second step of Stone duality for spectral locales
#270
ayberkt
closed
1 month ago
4
Add alternative definition of the notion of distributive lattice isomorphism
#269
ayberkt
opened
2 months ago
0
Prove that every spectral frame is isomorphic to the frame of ideals of its lattice of compact opens
#268
ayberkt
closed
1 month ago
0
Transportation of distributive lattices along equivalences
#267
ayberkt
closed
2 months ago
1
First step of Stone duality for spectral locales
#266
ayberkt
closed
2 months ago
1
Fix Issue 263
#265
ayberkt
closed
2 months ago
1
Address review from PR #255
#264
ayberkt
closed
2 months ago
3
Remove completed TODO on the topology of Scott domains
#263
ayberkt
closed
2 months ago
3
[Aborted] First step towards Stone duality for spectral locales
#262
ayberkt
closed
2 months ago
4
Prove that isomorphic frames are equal
#261
ayberkt
closed
2 months ago
2
Prove that isomorphic frames are equal
#260
ayberkt
closed
2 months ago
1
Define frame isomorphisms
#259
ayberkt
closed
2 months ago
0
Prove that the locale of spectra is a spectral locale
#258
ayberkt
closed
2 months ago
0
Prove the universal property of the Sierpiński locale (depends on PR #256)
#257
ayberkt
closed
3 months ago
0
Step 3 of PR #217 (depends on PR #255)
#256
ayberkt
closed
3 months ago
0
Step 2 of PR #217
#255
ayberkt
closed
3 months ago
4
Prove that the locale 2 is compact (depends on PR #253)
#254
ayberkt
closed
4 months ago
0
Define the discrete locale over a set
#253
ayberkt
closed
4 months ago
0
Define the homomorphism between lattices of compact opens given by a spectral map of locales
#252
ayberkt
closed
4 months ago
0
Prove that the locale of spectra is compact
#251
ayberkt
closed
4 months ago
0
Define the locale of spectra over a distributive lattice
#250
ayberkt
closed
4 months ago
0
Change files to lagda, add author and remove links
#249
tnttodda
closed
4 months ago
0
Define the distributive lattice of compact opens of a spectral locale
#248
ayberkt
closed
4 months ago
0
Next