martinescardo / typetopology Goto Github PK
View Code? Open in Web Editor NEWLogical manifestations of topological concepts, and other things, via the univalent point of view.
License: GNU General Public License v3.0
Logical manifestations of topological concepts, and other things, via the univalent point of view.
License: GNU General Public License v3.0
In PR #148, I mentioned that I completed a TODO that I saw in module EffectfulForcing.MFPSAndVariations.Continuity
. This was actually just one component of the problem mentioned in that TODO, the other half being the same thing for uniform continuity.
Now, to complete PR #210, I need to complete that other component of that TODO.
I realised that I’ve never ported the definition of a sublocale from ayberkt/formal-topology-in-UF
. It’s probably a good idea to do this.
A TODO that I saw in index.lagda
: add short explanations of each module.
Something we discussed with @martinescardo a while ago. Making an issue here so that I don't forget about it.
Currently, all Agda files in TypeTopology
have the .lagda
extension. For reasons that I don't really understand, Agda can generate Markdown files only from files with extension .lagda.md
. It is possible to generate HTML from .lagda
files but this has the problem that the literate parts of the code are treated as code (i.e. are not wrapped in <p></p>
tags) so it's not possible to make the formatting nice by adding a CSS file.
It seems that the best way to fix this is by converting .lagda
files to .lagda.md
files (in fact @martinescardo already wrote a script for this if I recall correctly). It would be great to make the HTML files generated from TypeTopology
nicer by doing this and compiling through a Markdown processor.
Request to port the PathSeq
functionality from the
PathSeq
library in https://github.com/HoTT/HoTT-Agda to
TypeTopology
. In HoTT-Agda the data structure PathSeq
is defined in lib.Base
, with auxiliary structure and data in lib.path-seq.*
.
Let us call a term p : x = y
a "path" from x
to y
. Abstract
path manipulation should have the following features:
A data structure to represent a path normalized concatenation. This is called an "abstract path."
If p
, q
, r
, s
, t
are paths, then, say, [p,q,r,s,t]
should be the corresponding abstract path, regardless of the parentheses. That is, p ∙ (q ∙ (r ∙ (s ∙ t)))
and (p ∙ q) ∙ (r ∙ (s ∙ t))
should ideally give rise to the same [p,q,r,s,t]
.
Path reasoning: equational-style reasoning for abstract path concatenation.
Conversion to and insertion from paths.
Abstract path equality, say, ==
Manipulation: if two abstract paths s
(resp. t
) contain
sub-(abstract) paths u
(resp. v
) and α : u == v
, we should
be able to write somethings of the form:
lemma : s == t
lemma = s ==⟨⟨ insertion-point | end-point | α ⟩⟩
t ==∎∎
In the above the insertion and the end points specify where u
occur
in s
. This should work even if u
and v
are of not of the same
length.
A TODO that I saw in the DomainTheory.Lifting.LiftingSetAlgebraic
module:
TODO: Show that freely adding a least element to a dcpo gives an algebraic dcpo
with a small compact basis if the original dcpo had a small compact basis.
(Do so in another file, e.g. LiftingDcpoAlgebraic.lagda).
@tomdjong: The index of the DomainTheory
development lists the TODO:
TypeTopology/source/DomainTheory/index.lagda
Lines 173 to 178 in 000d51a
and says
If you'd like to work on Item 4, please get in touch with Ayberk Tosun.
This has now been done (in PR #255) so we can remove this TODO (and maybe provide some pointers to the modules in which it has been done).
Now that the new version of Agda has been released, it might be a good idea to update the typechecking workflow to use that.
As discussed on Discord with @martinescardo, the formalisation of the winning strategy for the Hydra game would be a good addition to TypeTopology
.
I'm trying to define a QIIT with the following constructors:
data _⊥ (A : 𝓤 ̇ ) : 𝓥 ⁺ ⊔ 𝓤 ̇
data Leq (A : 𝓤 ̇ ) : A ⊥ → A ⊥ → 𝓥 ⁺ ⊔ 𝓤 ̇
data _⊥ A where
-- ...
lub : {I : 𝓥 ̇ } → (Σ α ꞉ (I → A ⊥) , is-directed (Leq A) α) → A ⊥
-- ...
data Leq A where
-- ...
lub-is-upperbound : {I : 𝓥 ̇ } {α : I → A ⊥} (δ : is-directed (Leq A) α)
(i : I) → Leq A (α i) (lub (α , δ))
-- ...
Agda does not accept these types, as it cannot verify that they're strictly positive. This has to do with the definition of is-directed
:
is-directed : {I : 𝓥 ̇ } {X : 𝓦' ̇ } (_⊑_ : X → X → 𝓣 ̇ ) → (I → X) → 𝓥 ⊔ 𝓣 ̇
is-directed {I = I} _⊑_ α =
∥ I ∥ ×
((i j : I) → ∥ Σ k ꞉ I , (α i ⊑ α k) × (α j ⊑ α k) ∥)
This causes Leq A
to occur inside of the propositional truncation, and as Agda only knows that ∥_∥
exists but knows nothing about how its elements may be constructed, Agda cannot verify that Leq A
occurs in a strictly positive place.
However, instead of just assuming that a propositional truncation type exists, we can also define it and only assume it's properties, like follows (I used postulate
here, but I would of course replace that with a modular approach if this makes it to a PR):
data ∥_∥' {𝓤 : Universe} (X : 𝓤 ̇ ) : 𝓤 ̇ where
∣_∣' : X → ∥ X ∥'
postulate
∥∥'-is-prop : {𝓤 : Universe} {X : 𝓤 ̇ } → is-prop ∥ X ∥'
∥∥'-rec : {𝓤 𝓥 : Universe} {X : 𝓤 ̇ } {P : 𝓥 ̇ } → is-prop P → (X → P) → ∥ X ∥' → P
It's easy to show that ∥_∥
and ∥_∥'
are equivalent and if I use ∥_∥'
in the definition of is-directed
, Agda will be able to typecheck the above QIIT.
It therefore seems to me that defining the propositional truncation and only assuming its properties, is preferred over assuming the whole type. Is this something we want to change in TypeTopology?
Continuation of #170.
There is a scriptcount-agda-files-and-lines
which I suggest everybody should run before their pull requests, and then update index.lagda
with this information.
Specifically, the snippet
* In our last count, on 2024.06.19, this development has 761 Agda
files with 215k lines of code, including comments and blank
lines. But we don't update the count frequently.
should perhaps always be updated in any pull request.
It would be even better if there was an automatic way of doing this.
Then we could omit "But we don't update the count frequently.".
Propositional + functional extensionality should be sufficient as @martinescardo pointed out.
In all modules which define it at the directory EffectfulForcing
.
Note: I'm creating this issue so that I don't forget about it. Nothing needs to be done about it for now.
The typechecking logs show a weird message
/entrypoint.sh: 37: [: true: unexpected operator
and I'm not sure why. Typechecking seems to be going fine though so this is probably nothing serious. In any case, I should take a look at why this is happening.
A long-standing TODO, discussed with @martinescardo before.
As discussed with @vrahli .
As pointed by @martinescardo at the meeting on 2024-04-30.
In module MLTT.List
, there is a notion called listed
.
TypeTopology/source/MLTT/List.lagda
Lines 101 to 102 in d8e2220
The propositional truncation of this should be equivalent to Kuratowski-finiteness. Proving this might be a fun exercise, but will involve some bureaucracy regarding the Fin
type.
As mentioned by @martinescardo on Discord.
Make sure that each of the following modules is properly commented:
AdjointFunctorTheoremForFrames.lagda
BooleanAlgebra.lagda
CharacterisationOfContinuity.lagda
ClassificationOfScottOpens.lagda
Clopen.lagda
CompactRegular.lagda
Compactness.lagda
Complements.lagda
Frame.lagda
GaloisConnection.lagda
HeytingComplementation.lagda
HeytingImplication.lagda
InitialFrame.lagda
NotationalConventions.lagda
Nucleus.lagda
PatchLocale.lagda
PatchOfOmega.lagda
PatchProperties.lagda
PerfectMaps.lagda
Regular.lagda
ScottContinuity.lagda
ScottLocale.lagda
Sierpinski.lagda
SmallBasis.lagda
Stone.lagda
StoneImpliesSpectral.lagda
UniversalPropertyOfPatch.lagda
WellInside.lagda
ZeroDimensionality.lagda
index.lagda
Properties.lagda
Spectrality.SpectralLocale.lagda
Spectrality.SpectralMap.lagda
Spectrality.SpectralityOfOmega.lagda
WayBelowRelation.Definition.lagda
WayBelowRelation.Properties.lagda
@ayberkt we should be consistent and use the same notational conventions as for \Sigma and \exists. So I suggest changing UF-Subsingleton-Combinators.lagda and any module that uses this syntax.
I just noticed the existence of the module frame.lagda
which I believe defines σ-frames.
Now that we have Frame.lagda
(added in #44), we should be a bit careful about the distinction between the two. As of now, the coexistence of multiple definitions that use the same name is a bit confusing.
The Dcpo
module contains the definitions of partial order, meet, join and so on.
TypeTopology/source/Dcpo.lagda
Lines 37 to 53 in e3835af
I am now working on implementing the beginnings of locale theory in TypeTopology
for which I need these definitions.
Would it be okay to separate these out into a module of their own or was this perhaps deliberately avoided for the sake of self-containment?
It seems that in
TypeTopology/source/UF-Subsingleton-Combinators.lagda
Lines 54 to 55 in 5f35dfc
and
TypeTopology/source/UF-Subsingleton-Combinators.lagda
Lines 125 to 126 in 5f35dfc
I accidentally used the wrong unicode character. I need to fix this at some point.
It is often convenient to have combinators for Ω, for instance
_∧_ : Ω 𝓤 → Ω 𝓥 → Ω (𝓤 ⊔ 𝓥)
P ∧ Q = (P holds × Q holds) , γ
where
γ = ×-is-prop (holds-is-prop P) (holds-is-prop Q)
agda/cubical has these defined in this module. It might be a good idea to do something similar in TypeTopology
.
Another TODO, analogous to #168.
As pointed out by @tomdjong, and discussed with @martinescardo.
In Negation.lagda
, the usual definition of decidability for a type is given:
TypeTopology/source/Negation.lagda
Lines 42 to 43 in f2c26d4
Would it be possible, in Agda, to express the notion of a semidecidable type so that the decidability of type A
is (at least) logically equivalent to the conjunction of semidecidability and co-semidecidability of A
?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.