Mercurial > hg > Members > kono > Proof > ZF-in-agda
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 = {!!}