Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison src/PFOD.agda @ 1096:55ab5de1ae02
recovery
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 23 Dec 2022 12:54:05 +0900 |
parents | e787d37d27a0 |
children | c2501d308c95 |
comparison
equal
deleted
inserted
replaced
1095:08b6aa6870d9 | 1096:55ab5de1ae02 |
---|---|
128 | 128 |
129 ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω) ≡ i1 → X ∋ i | 129 ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω) ≡ i1 → X ∋ i |
130 ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω)) | 130 ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω)) |
131 ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p | 131 ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p |
132 | 132 |
133 open _⊆_ | |
134 | |
135 -- someday ... | 133 -- someday ... |
136 -- postulate | 134 -- postulate |
137 -- ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X | 135 -- ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt ) =h= X |
138 -- fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f | 136 -- fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f |
139 | 137 |