# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564142886 -32400
# Node ID 6e778b0a720244cb0575317836fd9ce5cf4d3c73
# Parent  540b845ea2de0db2b7b8df99cd94898212437715
add filter

diff -r 540b845ea2de -r 6e778b0a7202 OD.agda
--- a/OD.agda	Thu Jul 25 14:42:19 2019 +0900
+++ b/OD.agda	Fri Jul 26 21:08:06 2019 +0900
@@ -198,7 +198,7 @@
 -- Axiom of choice in intutionistic logic implies the exclude middle
 --     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
 --
-p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )
+p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )         -- assuming axiom of choice
 p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } ))
 p∨¬p {n} p | yes eq = case2 (¬p eq) where
    ps = record { def = λ x → p }
@@ -213,13 +213,13 @@
    lemma : ps ∋ minimul ps (λ eq →  ¬p (eqo∅ eq)) 
    lemma = x∋minimul ps (λ eq →  ¬p (eqo∅ eq))
 
-∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p 
+∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p   -- assuming axiom of choice    
 ∋-p {n} p with p∨¬p p
 ∋-p {n} p | case1 x = yes x
 ∋-p {n} p | case2 x = no x
 
 double-neg-eilm : {n  : Level } {A : Set (suc n)} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm {n} {A} notnot with ∋-p  A
+double-neg-eilm {n} {A} notnot with ∋-p  A                         -- assuming axiom of choice
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
@@ -243,6 +243,24 @@
 Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   -- Ord x does not help ord-power→
 
+
+_⊆_ : {n : Level} ( A B : OD {suc n}  ) → ∀{ x : OD {suc n} } →  Set (suc n)
+_⊆_ A B {x} = A ∋ x →  B ∋ x
+
+infixr  220 _⊆_
+
+subset-lemma : {n : Level} → {A x y : OD {suc n} } → (  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( _⊆_ x A {y} )
+subset-lemma {n} {A} {x} {y} = record {
+      proj1 = λ z lt → proj1 (z  lt)
+    ; proj2 = λ x⊆A lt → record { proj1 = x⊆A lt ; proj2 = lt }
+   } 
+
+Def=A→Set : {n : Level} → (A  :  Ordinal {suc n}) → Def (Ord A) == record { def = λ x → x o< A → Set n  }
+Def=A→Set {n} A  = record {
+              eq→ = λ {y} DAx y<A →  {!!}
+        ;  eq← = {!!} -- λ {y} f → {!!}
+    } where
+
 -- Constructible Set on α
 -- Def X = record { def = λ y → ∀ (x : OD ) → y < X ∧ y <  od→ord x } 
 -- L (Φ 0) = Φ
@@ -285,8 +303,6 @@
     Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
-    _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
-    _⊆_ A B {x} = A ∋ x →  B ∋ x
     Power : OD {suc n} → OD {suc n}
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     ｛_｝ : ZFSet → ZFSet
@@ -302,7 +318,6 @@
 
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    infixr  220 _⊆_
     isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
@@ -446,6 +461,7 @@
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
                   lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
 
+         --  assuming axiom of choice
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = x∋minimul x not
diff -r 540b845ea2de -r 6e778b0a7202 filter.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/filter.agda	Fri Jul 26 21:08:06 2019 +0900
@@ -0,0 +1,65 @@
+open import Level
+module filter where
+
+open import zf
+open import ordinal
+open import OD
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+open import Relation.Binary
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+
+record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
+   field
+       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       G : OD {suc n}
+       G∋1 : G ∋ max
+       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  max 
+       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+
+dense :  {n : Level} → Set (suc (suc n))
+dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q ))
+
+open OD.OD
+
+-- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
+
+Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n}
+Pred {n} dom = record {
+      def = λ x → def dom x → Set n
+  }
+
+Hω2 : {n : Level} →  OD {suc n}
+Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
+
+_⊆_ : {n : Level} → ( A B : OD {suc n}  ) → ∀{ x : OD {suc n} } →  Set (suc n)
+_⊆_ A B {x} = A ∋ x →  B ∋ x
+
+Hω2Filter :   {n : Level} → Filter {n} Hω2 od∅
+Hω2Filter {n} = record {
+       _⊇_ = {!!}
+     ; G = {!!}
+     ; G∋1 = {!!}
+     ; Gmax = {!!}
+     ; Gless = {!!}
+     ; Gcompat = {!!}
+  } where
+       P = Hω2
+       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       _⊇_ = {!!}
+       G : OD {suc n}
+       G = {!!}
+       G∋1 : G ∋ od∅
+       G∋1 = {!!}
+       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  od∅
+       Gmax = {!!}
+       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gless = {!!}
+       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+       Gcompat = {!!}
+