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

changeset 637:c17d46ecb051

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 11:21:27 +0900
parents 844eb13a5a39
children 75578f19ed3c
files src/zorn.agda
diffstat 1 files changed, 14 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 21 11:03:20 2022 +0900
+++ b/src/zorn.agda	Tue Jun 21 11:21:27 2022 +0900
@@ -682,22 +682,25 @@
           → (ind :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : Ordinal)  →   ind  x (λ y _ → TransFinite ind  y )  ≡ TransFinite ind  x
 
-     record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) ( z : Ordinal ) : Set (Level.suc n) where
+     record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) : Set (Level.suc n) where
       field
-         zc : ZChain A y f z
+         zc : ZChain A y f (& A)
       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) 
+         chain-mono : {x y : Ordinal} → x o≤ y → supf x ⊆' supf y 
+         f-total : {x : Ordinal} → IsTotalOrderSet (supf x) 
 
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
-         → (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
+         → ZChain1 f mf ay 
+     SZ1 f mf {y} ay = record { zc = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) (& A)
              ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where
          sf : Ordinal → HOD
-         sf x = ZChain.supf (TransFinite (ind f mf ay) z) x
-         mono :  {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → w o≤ z → sf x ⊆' sf w 
-         mono {a} {b} sf a≤b b≤z = TransFinite0 {λ b → a o≤ b → b o≤ z →  sf a ⊆' sf b } {!!} b a≤b b≤z
+         sf x = ZChain.supf (TransFinite (ind f mf ay) (& A)) x
+         mono :  {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → sf x ⊆' sf w 
+         mono {a} {b} sf a≤b = TransFinite0 {λ b → a o≤ b → sf a ⊆' sf b } mind b a≤b where
+            mind :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o≤ y₁ → sf a ⊆' sf y₁) → a o≤ x → sf a ⊆' sf x
+            mind = {!!}
+
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -716,9 +719,9 @@
               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 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) (& A))
+         zorn04 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) )
          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 
+         total =  ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) 
 
 -- usage (see filter.agda )
 --