Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison generic-filter.agda @ 396:8c092c042093

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 27 Jul 2020 15:11:54 +0900
parents 77c6123f49ee
children 48ea49494fd1
comparison
equal deleted inserted replaced
395:77c6123f49ee 396:8c092c042093
132 132
133 open _==_ 133 open _==_
134 134
135 postulate f-extensionality : { n m : Level} → Relation.Binary.PropositionalEquality.Extensionality n m 135 postulate f-extensionality : { n m : Level} → Relation.Binary.PropositionalEquality.Extensionality n m
136 136
137 ω2f : (f : Nat → Two) → ω→2 ∋ fω→2 f 137 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
138 ω2f f = power← infinite (fω→2 f) (λ {x} lt → proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt)) 138 ω2∋f f = power← infinite (fω→2 f) (λ {x} lt → proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))
139 139
140 ω→2f≡i0 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω) ≡ i1 → X ∋ i
141 ω→2f≡i0 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
142 ω→2f≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) ? p
143
140 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X 144 ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X
141 ω→2f-iso X lt = record { 145 ω→2f-iso X lt = record {
142 eq→ = eq1 146 eq→ = eq1
143 ; eq← = eq2 147 ; eq← = eq2
144 } where 148 } where
145 eq1 : {x : Ordinal} → odef (fω→2 (ω→2f X lt)) x → odef X x 149 eq1 : {x : Ordinal} → odef (fω→2 (ω→2f X lt)) x → odef X x
146 eq1 {x} fx = {!!} 150 eq1 {x} fx = {!!} where
151 x-nat : odef infinite x
152 x-nat = subst (λ k → odef infinite k) diso ( ODC.double-neg-eilm O
153 (power→ infinite _ (ω2∋f (ω→2f X lt)) (d→∋ (fω→2 (ω→2f X lt)) fx )))
154 i : Nat
155 i = ω→nat (ord→od x) (d→∋ infinite x-nat)
156 is-i1 : ω→2f X lt i ≡ i1
157 is-i1 = {!!}
147 eq2 : {x : Ordinal} → odef X x → odef (fω→2 (ω→2f X lt)) x 158 eq2 : {x : Ordinal} → odef X x → odef (fω→2 (ω→2f X lt)) x
148 eq2 {x} Xx = {!!} 159 eq2 {x} Xx = {!!} where
160 x-nat : odef infinite x
161 x-nat = {!!}
149 162
150 fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2f f) ≡ f 163 fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
151 fω→2-iso f = f-extensionality (λ x → eq1 x ) where 164 fω→2-iso f = f-extensionality (λ x → eq1 x ) where
152 eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2f f) x ≡ f x 165 eq1 : (x : Nat) → ω→2f (fω→2 f) (ω2∋f f) x ≡ f x
153 eq1 x = {!!} 166 eq1 x = {!!}
154 167
155 168
156 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD 169 ↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
157 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) )) 170 ↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))