Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 629:5b7b54fa4cf7
... TFcomm
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 20 Jun 2022 16:23:55 +0900 |
| parents | 0b5ff1c7032c |
| children | d5cd551e0ed9 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 14 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jun 20 15:39:40 2022 +0900 +++ b/src/zorn.agda Mon Jun 20 16:23:55 2022 +0900 @@ -654,11 +654,22 @@ → (z : Ordinal) → (z<x : z o< x) → ZChain.chain (prev z z<x ) ⊆' ZChain.chain ( ind f mf ay x prev ) ind-mono f mf ay x prev z z<x = {!!} - SZ-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) -o {a b : Ordinal } → a o< b → + postulate + TFcomm : { ψ : Ordinal → Set (Level.suc n) } + → (ind : (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x ) + → ∀ (x : Ordinal) → ind x (λ y _ → TransFinite ind y ) ≡ TransFinite ind x + + SZ-mono : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y) + → {a b : Ordinal } → a o< b → ZChain.chain (TransFinite {λ z → ZChain A y f z } (ind f mf ay ) a ) ⊆' ZChain.chain (TransFinite {λ z → ZChain A y f z } (ind f mf ay ) b ) - SZ-mono f mf {y} ay = ? + SZ-mono f mf {y} ay {a} {b} a<b = TransFinite0 {λ b → a o< b → ZChain.chain (TransFinite {λ z → ZChain A y f z } (ind f mf ay ) a ) ⊆' + ZChain.chain (TransFinite {λ z → ZChain A y f z } (ind f mf ay ) b ) } sind b a<b where + sind : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o< y₁ → + ZChain.chain (TransFinite (ind f mf ay) a) ⊆' ZChain.chain (TransFinite (ind f mf ay) y₁)) → + a o< x → ZChain.chain (TransFinite (ind f mf ay) a) ⊆' ZChain.chain (TransFinite (ind f mf ay) x) + sind = {!!} -- + zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM