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

changeset 639:18e45e419a68

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 Fri, 24 Jun 2022 13:29:11 +0900
parents 6cd4a483122c
children 4f48fe1b884a
files src/zorn.agda
diffstat 1 files changed, 8 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 21 08:46:26 2022 +0900
+++ b/src/zorn.agda	Fri Jun 24 13:29:11 2022 +0900
@@ -691,7 +691,7 @@
 
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
          → (z : Ordinal) → ZChain1 ( λ y → ZChain.chain (TransFinite (ind f mf ay ) y) ) z
-     SZ1 f mf {y} ay z = TransFinite {λ w → ZChain1 ( λ y → ZChain.chain (TransFinite (ind f mf ay ) y) ) w} indp z where
+     SZ1 f mf {y} ay z = TransFinite {λ w → {!!} w} {!!} z where
          indp :  (x : Ordinal) →
             ((y₁ : Ordinal) → y₁ o< x → ZChain1 (λ y₂ → ZChain.chain (TransFinite (ind f mf ay) y₂)) y₁) →
             ZChain1 (λ y₁ → ZChain.chain (TransFinite (ind f mf ay) y₁)) x
@@ -706,6 +706,13 @@
          ... | tri≈ ¬a b ¬c = {!!}
          ... | tri> ¬a ¬b y<x = {!!}
 
+     T⊆ : { ψ : Ordinal  → HOD }
+          → ( (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → {z : Ordinal} → z o≤ y  → ψ z ⊆' ψ y ) → {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x ) 
+          →  ∀ (x : Ordinal)  → {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x 
+     T⊆ {ψ} prev x {z} z≤x = TransFinite0 (λ x prev → indt x prev  ) x {z} z≤x where
+         indt : (x : Ordinal) → ( (y : Ordinal) → y o< x →  {z : Ordinal} → z o≤ y  → ψ z ⊆' ψ y ) →  {z : Ordinal} → z o≤ x  → ψ z ⊆' ψ x 
+         indt x prev {z} z≤x {i} zi = prev ? ? {z} z≤x zi
+
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where