martinescardo / typetopology Goto Github PK

Another TODO, analogous to #168.

It seems that in

and

I accidentally used the wrong unicode character. I need to fix this at some point.

In module MLTT.List, there is a notion called listed.

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.

A long-standing TODO, discussed with @martinescardo before.

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:

1. 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].

2. Path reasoning: equational-style reasoning for abstract path concatenation.

3. Conversion to and insertion from paths.

4. Abstract path equality, say, ＝＝

5. 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.

As pointed by @martinescardo at the meeting on 2024-04-30.

The Dcpo module contains the definitions of partial order, meet, join and so on.

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?

A TODO that I saw in index.lagda: add short explanations of each module.

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.

Propositional + functional extensionality should be sufficient as @martinescardo pointed out.

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.

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.

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.

In Negation.lagda, the usual definition of decidability for a type is given:

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?

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.

As mentioned by @martinescardo on Discord.

As pointed out by @tomdjong, and discussed with @martinescardo.

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

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?

In all modules which define it at the directory EffectfulForcing.

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 with @vrahli .

@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.

Dcpo analogue of a proof implemented in #180. Discussed with @tomdjong.

As discussed on Discord with @martinescardo, the formalisation of the winning strategy for the Hydra game would be a good addition to TypeTopology.

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.

Continuation of #170.

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:

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).