Define omega-regular cover spaces and real cover space

JetBrains · Mar 5, 2024 · 396dfc1 · 396dfc1
1 parent 818c480
commit 396dfc1
Show file tree

Hide file tree

Showing 6 changed files with 394 additions and 365 deletions.
diff --git a/src/Arith/Real.ard b/src/Arith/Real.ard
diff --git a/src/Set/Filter.ard b/src/Set/Filter.ard
@@ -1,3 +1,4 @@
+\import Logic
 \import Logic.Meta
 \import Order.Lattice
 \import Order.PartialOrder
@@ -15,6 +16,13 @@
 \record ProperFilter \extends SetFilter
   | isProper {U : Set X} : F U -> ∃ U
 
+\func pointFilter {X : \Set} (x : X) : ProperFilter X \cowith
+  | F U => U x
+  | filter-mono p => p
+  | filter-top => ()
+  | filter-meet p q => (p,q)
+  | isProper Ux => inP (x,Ux)
+
 \instance ProperFilterSemilattice (X : \Set) : MeetSemilattice (ProperFilter X)
   | <= F G => F ⊆ G
   | <=-refl c => c

diff --git a/src/Set/Subset.ard b/src/Set/Subset.ard
@@ -13,10 +13,10 @@
     \lemma single_<= {A : \Set} {a : A} {U : Set A} (Ua : U a) : single a ⊆ U
       => \lam p => rewriteI p Ua
 
-    \func Union {A : \hType} (S : Set (Set A)) : Set A
+    \func Union {A : \hType} (S : Set A -> \hType) : Set A
       => \lam a => ∃ (U : S) (U a)
 
-    \lemma Union-cond {A : \hType} {S : Set (Set A)} {U : Set A} (SU : S U) : U ⊆ Union S
+    \lemma Union-cond {A : \hType} {S : Set A -> \hType} {U : Set A} (SU : S U) : U ⊆ Union S
       => \lam Ux => inP (U,SU,Ux)
   }