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

changeset 616:fae0fa6184d5

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 Sat, 18 Jun 2022 00:07:25 +0900
parents 9ac3789bf058
children 50999e72f19f
files src/zorn.agda
diffstat 1 files changed, 10 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Jun 17 23:19:19 2022 +0900
+++ b/src/zorn.agda	Sat Jun 18 00:07:25 2022 +0900
@@ -420,7 +420,7 @@
                initial {i} (init ai) = case1 refl
                initial .{f x} (fsuc x lt) = {!!}
 
-     chain-mono : ( A : HOD )  {x y : Ordinal}  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) { a b : Ordinal }
+     chain-mono :  {x y : Ordinal} (ay : odef A y)  ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) { a b : Ordinal }
          → (zx : ZChain A y f a ) → (zy : ZChain A y f b)  → a o≤ b → b o< osuc x →  ZChain.chain zx ⊆' ZChain.chain zy
 
      --
@@ -623,7 +623,7 @@
          u-chain∋x :  odef Uz y
          u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ay ) }
          u-mono :  ( a b : Ordinal ) → b o< osuc x → a o< osuc b → (za : ZChain A y f a) (zb : ZChain A y f b) → ZChain.chain za  ⊆' ZChain.chain zb
-         u-mono a b b≤x a≤b za zb {i} zai = chain-mono A f mf za zb a≤b  b≤x zai
+         u-mono a b b≤x a≤b za zb {i} zai = chain-mono ay f mf za zb a≤b  b≤x zai
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
          ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)
@@ -633,16 +633,19 @@
          ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
             (ordtrans (UZFChain.u<x ux) <-osuc)  (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
 
-     ind-mono : (A : HOD) (x y : Ordinal ) {b : Ordinal } ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (zb : ZChain A y f b) →
+     zfx :  (x : Ordinal ) {y : Ordinal } (ay : odef A y ) ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A y f x
+     zfx x ay f mf = TransFinite {λ z → {y : Ordinal } → (ay : odef A y ) → ZChain A y f z } (ind f mf) x ay
+
+     ind-mono :  (x : Ordinal ) {y : Ordinal } (ay : odef A y ) {b : Ordinal } ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (zb : ZChain A y f b) →
              (a : Ordinal)
                 → ((c : Ordinal) → c o< a → c o≤ b → b o≤ x → (zc : ZChain A y f c) {i : Ordinal} → odef (ZChain.chain zc) i → odef (ZChain.chain zb) i)
                 → a o≤ b → b o≤ x → (za : ZChain A y f a) {i : Ordinal} → odef (ZChain.chain za) i → odef (ZChain.chain zb) i
-     ind-mono A x y {b} f mf zb a prev a≤b b≤x za {i} zai with Oprev-p a
+     ind-mono x {y} ay {b} f mf zb a prev a≤b b≤x za {i} zai with Oprev-p a
      ... | yes op = mc00 where
           open ZChain
           px = Oprev.oprev op
           zc0 : ZChain A y f (Oprev.oprev op)
-          zc0 = ?
+          zc0 = {!!} -- zfx (Oprev.oprev op) ay f mf
           mc00 : odef (chain zb) i
           mc00 with ODC.∋-p O A (* a)
           ... | no noax = {!!}
@@ -656,9 +659,9 @@
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b y<x = {!!}
 
-     chain-mono A {x} {y} f mf {a} {b} za zb a≤b b≤x = TransFinite {λ a →  
+     chain-mono {x} {y} ay f mf {a} {b} za zb a≤b b≤x = TransFinite {λ a →  
          a o≤ b → b o≤ x  → (za : ZChain A y f a) → {i : Ordinal } → odef (ZChain.chain za) i → odef (ZChain.chain zb) i }
-         (ind-mono A x y f mf zb) a a≤b b≤x za  
+         (ind-mono x ay f mf zb) a a≤b b≤x za  
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM