# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655714368 -32400
# Node ID d5cd551e0ed969271e2169294cc475e6f345e027
# Parent  5b7b54fa4cf70435ea21841903553b49491cf9d5
...

diff -r 5b7b54fa4cf7 -r d5cd551e0ed9 src/zorn.agda
--- a/src/zorn.agda	Mon Jun 20 16:23:55 2022 +0900
+++ b/src/zorn.agda	Mon Jun 20 17:39:28 2022 +0900
@@ -243,7 +243,6 @@
       chain∋x : odef chain x
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
       f-next : {a : Ordinal } → odef chain a → odef chain (f a)
-      f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
       is-max :  {a b : Ordinal } → (ca : odef chain a ) →  b o< osuc z  → (ab : odef A b) 
           → HasPrev A chain ab f ∨  IsSup A chain ab  
           → * a < * b  → odef chain b
@@ -400,6 +399,63 @@
      -- create all ZChains under o< x
      --
 
+     ys : {y : Ordinal} → (ay : odef A y)  (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD
+     ys {y} ay f mf = record { od = record { def = λ x →  FClosure A f y x  } ; odmax = & A ; <odmax = {!!} }
+     init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x
+     init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx →  A∋fc y f mf fx
+                     ; f-next = λ {x} sx → fsuc x sx  ; supf = λ _ → ys ay f mf 
+                     ; initial = {!!} ; chain∋x  = init ay ; is-max = is-max } where
+               i-total : IsTotalOrderSet (ys ay f mf )
+               i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb)
+               is-max : {a b : Ordinal} → odef (ys ay f mf) a →
+                    b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab →
+                    * a < * b → odef (ys ay f mf) b
+               is-max {a} {b} yca b≤x ab P a<b = {!!}
+               initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i
+               initial {i} (init ai) = case1 refl
+               initial .{f x} (fsuc x lt) = {!!}
+
+     sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
+         → ((z : Ordinal) → z o< x → HOD ) → HOD
+     sind f mf {y} ay x prev  with Oprev-p x
+     ... | yes op = sc4 where
+          px = Oprev.oprev op
+          sc : HOD
+          sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
+
+          sc4 : HOD
+          sc4 with ODC.∋-p O A (* x)
+          ... | no noax = {!!}
+          ... | yes ax with ODC.p∨¬p O ( HasPrev A sc ax f )   
+          ... | case1 pr = sc
+          ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A sc ax )
+          ... | case1 is-sup =  schain where
+                -- A∋sc -- x is a sup of zc 
+                sup0 : SUP A sc 
+                sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
+                        x21 :  {y : HOD} → sc ∋ y → (y ≡ * x) ∨ (y < * x)
+                        x21 {y} zy with IsSup.x<sup is-sup zy 
+                        ... | case1 y=x = case1 ( subst₂ (λ j k → j ≡ * k  ) *iso &iso ( cong (*) y=x)  )
+                        ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x  )
+                sp : HOD
+                sp = SUP.sup sup0 
+                schain : HOD
+                schain = record { od = record { def = λ x → odef sc x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!}  }
+          ... | case2 ¬x=sup =  sc
+     ... | no ¬ox with trio< x y
+     ... | tri< a ¬b ¬c = {!!}
+     ... | tri≈ ¬a b ¬c = {!!}
+     ... | tri> ¬a ¬b y<x = Uz where
+         record Usup (z : Ordinal) : Set n where -- Union of supf from y which has maximality o< x
+            field
+               u : Ordinal
+               u<x : u o< x
+               chain∋z : odef (prev u u<x ) z
+         Uz : HOD
+         Uz = record { od = record { def = λ y → Usup y } ; odmax = & A
+             ; <odmax = {!!} } -- λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) }
+
+
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
          → ((z : Ordinal) → z o< x → ZChain A y f z) → ZChain A y f x
      ind f mf {y} ay x prev with Oprev-p x
@@ -425,8 +481,7 @@
           no-extenion is-max = record { supf = supf0 ;  chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc)
                      ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc)
                      ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc) 
-                     ; f-immediate =  subst (λ k →  {x₁ : Ordinal} {y₁ : Ordinal} → odef k x₁ → odef k y₁ →
-                            ¬ (* x₁ < * y₁) ∧ (* y₁ < * (f x₁)) ) seq (ZChain.f-immediate zc) ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc)
+                     ; chain∋x  = subst (λ k → odef k y ) seq (ZChain.chain∋x  zc)
                              ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) →
                                  HasPrev A k ab f ∨  IsSup A k ab → * a < * b → odef k b  ) seq is-max } where
                 supf0 : Ordinal → HOD
@@ -466,7 +521,7 @@
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax )
           ... | case1 is-sup = -- x is a sup of zc 
                 record {  chain⊆A = {!!} ; f-next = {!!} 
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 } where
+                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!}   ; supf = supf0 } where
                 sup0 : SUP A (ZChain.chain zc) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -525,23 +580,6 @@
                 A∋za za = ZChain.chain⊆A zc za 
                 za<sup :  {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨  ( * a < sp )
                 za<sup za =  SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za )
-                simm : {a b : Ordinal}  → odef schain a → odef schain b → ¬ (* a < * b) ∧ (* b < * (f a))
-                simm {a} {b} (case1 za) (case1 zb) = ZChain.f-immediate zc za zb
-                simm {a} {b} (case1 za) (case2 sb) p with  proj1 (mf a (A∋za za) )
-                ... | case1 eq = <-irr (case2  (subst (λ k → * b < k ) (sym eq) (proj2 p))) (proj1 p) 
-                ... | case2 a<fa with za<sup  ( ZChain.f-next zc za ) | s≤fc (& sp) f mf sb
-                ... | case1 fa=sp | case1 sp=b = <-irr (case1 (trans fa=sp (trans (sym *iso) sp=b )) ) ( proj2 p )
-                ... | case2 fa<sp | case1 sp=b = <-irr (case2 fa<sp) (subst (λ k → k < * (f a) ) (trans (sym sp=b) *iso) (proj2 p ) )
-                ... | case1 fa=sp | case2 sp<b = <-irr (case2 (proj2 p )) (subst  (λ k → k < * b) (sym fa=sp) (subst (λ k → k < * b ) *iso sp<b ) )
-                ... | case2 fa<sp | case2 sp<b = <-irr (case2 (proj2 p )) (ptrans fa<sp (subst (λ k → k < * b ) *iso sp<b ) )
-                simm {a} {b} (case2 sa) (case1 zb) p with  proj1 (mf a ( subst (λ k → odef A k) &iso ( A∋schain (case2 (subst (λ k → FClosure A f (& sp) k ) (sym &iso) sa) )) ) )
-                ... | case1 eq = <-irr (case2  (subst (λ k → * b < k ) (sym eq) (proj2 p))) (proj1 p) 
-                ... | case2 b<fb with  s≤fc (& sp) f mf sa | za<sup zb
-                ... | case1 sp=a | case1 b=sp = <-irr (case1 (trans b=sp (trans (sym *iso) sp=a )) ) (proj1 p )
-                ... | case1 sp=a | case2 b<sp = <-irr (case2 (subst (λ k → * b < k ) (trans (sym *iso) sp=a)  b<sp ) ) (proj1 p )
-                ... | case2 sp<a | case1 b=sp = <-irr (case2 (subst ( λ  k → k < * a ) (trans *iso (sym b=sp)) sp<a  )) (proj1 p )
-                ... | case2 sp<a | case2 b<sp = <-irr (case2 (ptrans b<sp (subst (λ k → k < * a) *iso sp<a ))) (proj1 p )
-                simm {a} {b} (case2 sa) (case2 sb) p = fcn-imm {A} (& sp) {a} {b} f mf sa sb p
                 s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b)
                     → HasPrev A schain ab f ∨ IsSup A schain ab   
                     → * a < * b → odef schain b
@@ -593,8 +631,11 @@
                 ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } )
                 ... | case2 b=sup = ⊥-elim ( ¬x=sup record { 
                       x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy)  } ) 
-     ... | no ¬ox = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} 
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} }   where --- limit ordinal case
+     ... | no ¬ox with trio< x y
+     ... | tri< a ¬b ¬c = init-chain ay f mf {!!}
+     ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
+     ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} 
+                     ; initial = {!!} ; chain∋x  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
                u : Ordinal
@@ -612,7 +653,7 @@
          u-initial :  {z : Ordinal} → odef Uz z → * y ≤ * z 
          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 = {!!} ; chain∋z = ZChain.chain∋x (prev y {!!} ) }
+         u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ) }
          supf0 : Ordinal → HOD
          supf0 z with trio< z x
          ... | tri< a ¬b ¬c = ZChain.supf (prev z a ) z
@@ -664,11 +705,11 @@
          ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) a )  ⊆' 
          ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) b )
      SZ-mono f mf {y} ay {a} {b} a<b = TransFinite0 {λ b → a o< b →  ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) a )  ⊆'
-         ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) b ) } sind b a<b where
-          sind :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o< y₁ →
+         ZChain.chain (TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) b ) } szind b a<b where
+          szind :  (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o< y₁ →
              ZChain.chain (TransFinite (ind f mf ay) a) ⊆' ZChain.chain (TransFinite (ind f mf ay) y₁)) →
             a o< x → ZChain.chain (TransFinite (ind f mf ay) a) ⊆' ZChain.chain (TransFinite (ind f mf ay) x)
-          sind = {!!}  --
+          szind = {!!}  --
 
 
      zorn00 : Maximal A