# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565938409 -32400
# Node ID 650bdad5672926d79698755cf9e45473832f7b3b
# Parent  846e0926bb89eeec474bd242e1649fdc2cf94a0c
...

diff -r 846e0926bb89 -r 650bdad56729 cardinal.agda
--- a/cardinal.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/cardinal.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -27,7 +27,7 @@
 <_,_> : (x y : OD) → OD
 < x , y > = (x , x ) , (x , y )
 
-record SetProduct ( A B : OD ) (x : Ordinal ) : Set n where
+record SetProduct ( A B : OD )  : Set n where
    field
       π1 : Ordinal
       π2 : Ordinal
@@ -43,7 +43,7 @@
 ∋-p A x | case2 t = no t
 
 _⊗_  : (A B : OD) → OD
-A ⊗ B  = record { def = λ x → SetProduct A B x }
+A ⊗ B  = record { def = λ x → SetProduct A B  }
 -- A ⊗ B  = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
 
 --  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
@@ -63,9 +63,27 @@
    ... | yes _ = π2 t
    ... | no _ = o∅
 
+
 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
 func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
 
+record Func←cd { dom cod : OD } {f : Ordinal } (f<F :  def (Func dom cod ) f) : Set n where
+   field
+      func-1 : Ordinal → Ordinal
+      func→od∈Func-1 :  (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋  func→od func-1 dom
+ 
+func←od1 : { dom cod : OD } → {f : Ordinal }  → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
+func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
+   lemma : Ordinal → Ordinal → Ordinal
+   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma x y | p | no n  = o∅
+   lemma x y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
+   ... | t with decp ( x  ≡ π1 t )
+   ... | yes _ = π2 t
+   ... | no _ = o∅
+
+func→od∈Func :  (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom 
+func→od∈Func f dom  = record { proj1 = {!!} ; proj2 = {!!} }
 
 -- contra position of sup-o<
 --
diff -r 846e0926bb89 -r 650bdad56729 filter.agda
--- a/filter.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/filter.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -1,8 +1,10 @@
 open import Level
-open import OD
+open import Ordinals
+module filter {n : Level } (O : Ordinals {n})   where
+
 open import zf
-open import ordinal
-module filter ( n : Level )  where
+open import logic
+import OD 
 
 open import Relation.Nullary
 open import Relation.Binary
@@ -12,23 +14,28 @@
 open import  Relation.Binary.PropositionalEquality
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 
-od = OD→ZF {n}
-
+open inOrdinal O
+open OD O
+open OD.OD
 
-record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
+open _∧_
+open _∨_
+open Bool
+
+record Filter  ( P max : OD  )  : Set (suc n) where
    field
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
-       G : OD {suc n}
+       _⊇_ : OD  → OD  → Set n
+       G : OD 
        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 )))
+       Gmax : { p : OD  } → P ∋ p → p ⊇  max 
+       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  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 ))
+dense :   Set (suc n)
+dense = { D P p : OD  } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q ))
 
-record NatFilter {n : Level} ( P : Nat → Set n)  : Set (suc n) where
+record NatFilter  ( P : Nat → Set n)  : Set (suc n) where
    field
        GN : Nat → Set n
        GN∋1 : GN 0
@@ -46,16 +53,16 @@
 
 -- 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
+Pred :  ( Dom : OD  ) → OD 
+Pred  dom = record {
+      def = λ x → def dom x → {!!}
   }
 
-Hω2 : {n : Level} →  OD {suc n}
-Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
+Hω2 :   OD 
+Hω2  = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) }
 
-Hω2Filter :   {n : Level} → Filter {n} Hω2 od∅
-Hω2Filter {n} = record {
+Hω2Filter :     Filter  Hω2 od∅
+Hω2Filter  = record {
        _⊇_ = _⊇_
      ; G = {!!}
      ; G∋1 = {!!}
@@ -64,17 +71,17 @@
      ; Gcompat = {!!}
   } where
        P = Hω2
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       _⊇_ : OD  → OD  → Set n
        _⊇_ = {!!}
-       G : OD {suc n}
+       G : OD 
        G = {!!}
        G∋1 : G ∋ od∅
        G∋1 = {!!}
-       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  od∅
+       Gmax : { p : OD  } → P ∋ p → p ⊇  od∅
        Gmax = {!!}
-       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gless : { p q : OD  } → 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 : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
        Gcompat = {!!}
 
diff -r 846e0926bb89 -r 650bdad56729 ordinal.agda
--- a/ordinal.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/ordinal.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -204,21 +204,6 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
--- we cannot prove this in intutionistic logic 
---  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
--- postulate 
---  TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
---   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
---   → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
---   → p
---
--- Instead we prove
---
-TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
-  → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → ¬ p )
-  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
-  → ¬ p
-TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
 open import Ordinals 
 
diff -r 846e0926bb89 -r 650bdad56729 zf.agda
--- a/zf.agda	Thu Aug 15 04:51:24 2019 +0900
+++ b/zf.agda	Fri Aug 16 15:53:29 2019 +0900
@@ -34,7 +34,7 @@
   _∩_ : ( A B : ZFSet  ) → ZFSet
   A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easer
+  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easier
   ｛_｝ : ZFSet → ZFSet
   ｛ x ｝ = ( x ,  x )
   infixr  200 _∈_