diff generic-filter.agda @ 396:8c092c042093

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Jul 2020 15:11:54 +0900
parents 77c6123f49ee
children 48ea49494fd1
line wrap: on
line diff
--- a/generic-filter.agda	Mon Jul 27 09:29:41 2020 +0900
+++ b/generic-filter.agda	Mon Jul 27 15:11:54 2020 +0900
@@ -134,22 +134,35 @@
 
 postulate f-extensionality : { n m : Level}  → Relation.Binary.PropositionalEquality.Extensionality n m
 
-ω2f : (f : Nat → Two) → ω→2 ∋ fω→2 f
-ω2f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
- 
+ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
+ω2∋f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
+
+ω→2f≡i0 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
+ω→2f≡i0 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
+ω→2f≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) ? p
+
 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
 ω→2f-iso X lt = record {
      eq→ = eq1
    ; eq← = eq2
   } where
      eq1 : {x : Ordinal} → odef (fω→2 (ω→2f X lt)) x → odef X x
-     eq1 {x} fx = {!!}
+     eq1 {x} fx = {!!} where
+         x-nat : odef infinite x
+         x-nat =  subst (λ k → odef infinite k) diso ( ODC.double-neg-eilm O
+             (power→ infinite _ (ω2∋f (ω→2f X lt)) (d→∋ (fω→2 (ω→2f X lt)) fx ))) 
+         i : Nat
+         i = ω→nat (ord→od x) (d→∋ infinite x-nat)
+         is-i1 : ω→2f X lt i ≡ i1
+         is-i1 = {!!}
      eq2 : {x : Ordinal} → odef X x → odef (fω→2 (ω→2f X lt)) x
-     eq2 {x} Xx = {!!}
+     eq2 {x} Xx = {!!} where
+         x-nat : odef infinite x
+         x-nat = {!!}
   
-fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2f f) ≡ f
+fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
 fω→2-iso f = f-extensionality (λ x → eq1 x ) where
-     eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2f f) x ≡ f x
+     eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2∋f f) x ≡ f x
      eq1 x = {!!}