Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison generic-filter.agda @ 410:6dcea4c7cba1
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 29 Jul 2020 12:42:05 +0900 |
parents | 48ea49494fd1 |
children | 6eaab908130e |
comparison
equal
deleted
inserted
replaced
409:3fba5f805e50 | 410:6dcea4c7cba1 |
---|---|
137 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f | 137 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f |
138 ω2∋f 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 | 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ω)) | 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 | 142 ω→2f≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p |
143 | 143 |
144 ω→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 |
145 ω→2f-iso X lt = record { | 145 ω→2f-iso X lt = record { |
146 eq→ = eq1 | 146 eq→ = eq1 |
147 ; eq← = eq2 | 147 ; eq← = eq2 |