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

changeset 635:761bf71e5594

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 Tue, 21 Jun 2022 10:07:58 +0900
parents fd7dc6277480
children 844eb13a5a39
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 21 09:45:12 2022 +0900
+++ b/src/zorn.agda	Tue Jun 21 10:07:58 2022 +0900
@@ -680,20 +680,24 @@
           → (ind :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : Ordinal)  →   ind  x (λ y _ → TransFinite ind  y )  ≡ TransFinite ind  x
 
-     record ZChain1 (supf : (z : Ordinal ) → HOD ) ( z : Ordinal ) : Set (Level.suc n) where
+     record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
+      field
+         zc : ZChain A y f z
+      supf = ZChain.supf zc 
       field
          chain-mono : {x y : Ordinal} → x o≤ y → y o≤ z →  supf x ⊆' supf y 
          f-total : {x : Ordinal} → x o≤ z → IsTotalOrderSet (supf x) 
 
      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 = {!!} where -- TransFinite {λ w → ZChain1 ( λ y → ZChain.chain (TransFinite (ind f mf ay ) y) ) w} indp z where
+         → (z : Ordinal) → ZChain1 f mf ay z
+     SZ1 f mf {y} ay z = record { zc = TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) z
+             ; chain-mono = {!!} ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp 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
+            ((y₁ : Ordinal) → y₁ o< x → ZChain1 f mf ay y₁) →
+            ZChain1 f mf ay x
          indp x prev with Oprev-p x
          ... | yes op  = sz02 where
-             sz02 : ZChain1 (λ y₁ → ZChain.chain (TransFinite (ind f mf ay) y₁)) x
+             sz02 : ZChain1 f mf ay x
              sz02 with ODC.∋-p O A (* x)
              ... | no noax = {!!}
              ... | yes noax = {!!}
@@ -719,7 +723,7 @@
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               zc5 = ⟪  Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫
          zorn04 : ZChain A (& s) (cf nmx) (& A)
-         zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
+         zorn04 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) (& A))
          total : IsTotalOrderSet (ZChain.chain zorn04)
          total =  ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) (& A)) o≤-refl