# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655475559 -32400
# Node ID 9ac3789bf058d07c904943e51b5f243daf29321a
# Parent  9bdb671cbffd6c2d368c2518801d48e15f3a5d4f
ind-mono

diff -r 9bdb671cbffd -r 9ac3789bf058 src/zorn.agda
--- a/src/zorn.agda	Tue Jun 14 18:24:17 2022 +0900
+++ b/src/zorn.agda	Fri Jun 17 23:19:19 2022 +0900
@@ -420,6 +420,9 @@
                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 }
+         → (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
+
      --
      -- create all ZChains under o< x
      --
@@ -619,51 +622,44 @@
          u-initial {z} u = ZChain.initial ( uzc u )  (UZFChain.chain∋z u)
          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< 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 = TransFinite0 {λ i → odef (chain za) i → odef (chain zb) i } uind i zai where
-            open ZChain
-            uind :  (i : Ordinal)
-                 → ((j : Ordinal) → j o< i →  odef (chain za) j → odef (chain zb) j)
-                 → odef (chain za) i → odef (chain zb) i
-            uind i previ zai = um01 where
-                FC : Fc∨sup A (chain⊆A za (chain∋x za)) f (& (chain za)) a i
-                FC = fc∨sup za zai
-                um01 : odef (chain zb) i
-                um01 with FC
-                ... | Finit i=y = subst (λ k → odef (chain zb) k ) (sym i=y) ( chain∋x zb )
-                ... | Fsup {p} {i} p<i pFC sup i≤b  = cb∋i where
-                     i-asup : (z : Ordinal) → FClosure A f p z → * z < * i
-                     i-asup = FSup.sup sup
-                     um06 : odef (chain za) p
-                     um06 = subst (λ k → odef k p ) *iso ( FSup.chain∋p sup )
-                     -- FClosure A f p is a subset of chain zb
-                     um07 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2
-                     um07 i2 (init ap ) = previ p p<i um06  
-                     um07 i (fsuc j fc) = f-next zb ( um07 j fc )
-                     um08 : odef (chain zb) p
-                     um08 = previ p p<i um06
-                     cl : HOD
-                     cl = record { od = record { def = λ x → FClosure A f p x } ; odmax = & A ; <odmax = cl<A } where
-                         cl<A : {i2 : Ordinal} → FClosure A f p i2 → i2 o< & A
-                         cl<A {i2} cl = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (A∋fc p f mf cl) ) )
-                     cb∋i : odef (chain zb) i
-                     cb∋i = ZChain.chain∋sup zb cl (λ {i2} lt → um07 i2 lt) (chain⊆A za zai) {!!} record { x<sup = λ {i2} cl → case2 (i-asup i2 cl) } 
-                ... | Fc {p} {i} p<i pFC FC with (FChain.fc∨sup FC) 
-                ... | fc = um02 i fc where
-                     um02 : (i2 : Ordinal) → FClosure A f p i2 → odef (chain zb) i2
-                     um02 i2 (init ap ) = previ p p<i um04  where
-                        um04 : odef (chain za) p
-                        um04 = subst (λ k → odef k p ) *iso ( FChain.chain∋p FC )
-                     um02 i (fsuc j fc) = f-next zb ( um02 j fc )
+         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-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)
-            (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+            (ordtrans (UZFChain.u<x uy) <-osuc) (ordtrans a <-osuc ) (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
          ... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-            (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy))
+            (ordtrans (UZFChain.u<x ux) <-osuc)  (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy))
          ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
-            (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
-         
+            (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) →
+             (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
+     ... | yes op = mc00 where
+          open ZChain
+          px = Oprev.oprev op
+          zc0 : ZChain A y f (Oprev.oprev op)
+          zc0 = ?
+          mc00 : odef (chain zb) i
+          mc00 with ODC.∋-p O A (* a)
+          ... | no noax = {!!}
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc0) ax f )
+          ... | case1 pr = {!!}
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
+          ... | case1 is-sup = {!!} -- x is a sup of zc0 
+          ... | case2 ¬x=sup  = {!!}
+     ... | no ¬ox with trio< x y
+     ... | tri< a ¬b ¬c = {!!}
+     ... | 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 →  
+         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  
+
      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