# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655677217 -32400
# Node ID 7ddb909eb9ab01fc0ececf4327fd2bea1ebe2006
# Parent  267a44ce18b5a6c10a30c93504ebf9c2e9c2cf83
dead end

diff -r 267a44ce18b5 -r 7ddb909eb9ab src/OrdUtil.agda
--- a/src/OrdUtil.agda	Sun Jun 19 13:24:53 2022 +0900
+++ b/src/OrdUtil.agda	Mon Jun 20 07:20:17 2022 +0900
@@ -264,14 +264,6 @@
     os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
     os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
 
-TransFiniteInd : { ψ : Ordinal  → Set (suc n) }
-          → { prop :  ( (x : Ordinal)  → ψ x)  → Ordinal  → Set (suc n) }
-          → ( ind  :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
-          → ( pind :  (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → prop (TransFinite {ψ} ind) y ) → prop (TransFinite {ψ} ind) x )
-          →  (x : Ordinal) -> prop (TransFinite {ψ} ind) x
-TransFiniteInd {ψ} {prop} ind pind  = {!!}
-
-
 module o≤-Reasoning {n : Level}  (O : Ordinals {n} )  where
 
     -- open inOrdinal O
diff -r 267a44ce18b5 -r 7ddb909eb9ab src/zorn.agda
--- a/src/zorn.agda	Sun Jun 19 13:24:53 2022 +0900
+++ b/src/zorn.agda	Mon Jun 20 07:20:17 2022 +0900
@@ -240,13 +240,17 @@
       chain⊆A : chain ⊆' A
       chain∋x : odef chain x
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
-      f-total : IsTotalOrderSet chain 
       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
 
+record ZChainT ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where
+   field
+      zc :    ZChain A x f z
+      total : IsTotalOrderSet (ZChain.chain zc)
+
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -317,12 +321,12 @@
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
      zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A (& s) f (& A) ) → SUP A  (ZChain.chain zc) 
-     zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc  )   
+     zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) {!!}   
      A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx)  (& A) ) 
         →  A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ))
      A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal  (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )
      sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) → SUP A (ZChain.chain zc)
-     sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) (ZChain.f-total zc) 
+     sp0 f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) {!!} 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
      zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y)
 
@@ -335,7 +339,7 @@
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
-              →  HasPrev A chain ab f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b )
+              →  HasPrev A chain ab f ∨  IsSup A chain {b} ab -- (supO  chain  (ZChain.chain⊆A zc) ? ≡ b )
               → * a < * b  → odef chain b
            z10 = ZChain.is-max zc
            z11 : & (SUP.sup sp1) o< & A
@@ -357,20 +361,21 @@
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
                    -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
-           z14 with ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
-           ... | tri< a ¬b ¬c = ⊥-elim z16 where
-               z16 : ⊥
-               z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
-               ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
-               ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
-           ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
-           ... | tri> ¬a ¬b c = ⊥-elim z17 where
-               z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
-               z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
-               z17 : ⊥
-               z17 with z15
-               ... | case1 eq = ¬b eq
-               ... | case2 lt = ¬a lt
+           z14 = {!!}
+           -- z14 with ? -- ZChain.f-total zc  (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           -- ... | tri< a ¬b ¬c = ⊥-elim z16 where
+           --     z16 : ⊥
+           --     z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
+           --     ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
+           --     ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
+           -- ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
+           -- ... | tri> ¬a ¬b c = ⊥-elim z17 where
+           --     z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
+           --     z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+           --     z17 : ⊥
+           --     z17 with z15
+           --     ... | case1 eq = ¬b eq
+           --     ... | case2 lt = ¬a lt
 
      -- ZChain contradicts ¬ Maximal
      --
@@ -426,7 +431,7 @@
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
                  record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
-                     ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 
+                     ; f-next =  ZChain.f-next zc0 
                      ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 }  where -- no extention
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc0) ab f ∨  IsSup A (ZChain.chain zc0) ab →
@@ -444,7 +449,7 @@
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
                 ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
                 zc9 :  ZChain A y f x
-                zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
+                zc9 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-next =  ZChain.f-next zc0 -- no extention
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 }
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is the min sup of zc0 
@@ -487,7 +492,7 @@
                         a<b : a < b
                         a<b = ptrans  (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b )
                 scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a )
-                scmp (case1 za) (case1 zb) = ZChain.f-total zc0 za zb
+                scmp (case1 za) (case1 zb) = {!!} -- total zc0 za zb
                 scmp {a} {b} (case1 za) (case2 fb) = cmp za fb 
                 scmp  (case2 fa) (case1 zb) with  cmp zb fa
                 ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq))  a
@@ -549,7 +554,7 @@
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc0 )
                      ... | case2 y<b  = ZChain.is-max zc0 (ZChain.chain∋x zc0 ) (zc0-b<x b b<x) ab (case2 (z24 p)) y<b
           ... | case2 ¬x=sup =  -- x is not f y' nor min-sup of former ZChain from y
-                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0  
+                   record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-next = ZChain.f-next zc0  
                      ; initial = ZChain.initial zc0 ; f-immediate = ZChain.f-immediate zc0 ; chain∋x  =  ZChain.chain∋x zc0 ; is-max = z18 }  where
                       -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -566,7 +571,7 @@
      ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!}
      ... | tri> ¬a ¬b y<x = UnionZ where
        UnionZ : ZChain A y f x
-       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next 
+       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-next = u-next 
                      ; initial = u-initial ; f-immediate = {!!} ; 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
@@ -625,14 +630,24 @@
          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 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)
-            (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)
-            (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)
-            (ordtrans (UZFChain.u<x ux) <-osuc)  (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
+         -- 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)
+         --    (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)
+         --    (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)
+         --    (ordtrans (UZFChain.u<x ux) <-osuc)  (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
+
+     zchain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → {y : Ordinal} (ya : odef A y) → ZChain A y f x 
+     zchain f mf x ya = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) x ya
+
+     ind-total : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  → (x : Ordinal) → 
+            ((z : Ordinal) → z o< x → {y : Ordinal} → odef A y → ZChainT A y f z) → {y : Ordinal} → odef A y → ZChainT A y f x
+     ind-total f mf x prev {y} ya = ?
+
+     zchain-total : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → {y : Ordinal} (ya : odef A y) → ZChainT A y f x
+     zchain-total f mf x {y} ya = TransFinite { λ z → {y : Ordinal } → (ya : odef A y ) → ZChainT A y f z } (ind-total f mf ) x {y} ya 
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM