Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff 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 |
line wrap: on
line diff
--- a/generic-filter.agda Wed Jul 29 00:25:07 2020 +0900 +++ b/generic-filter.agda Wed Jul 29 12:42:05 2020 +0900 @@ -139,7 +139,7 @@ ω→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≡i0 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X ω→2f-iso X lt = record {