# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656888090 -32400
# Node ID 1002866230b8d4a450d83d34b2a9a2db11ac7a34
# Parent  6a8d13b02a508e5d38259077062931f63088e5c9
new TransFinite induction

diff -r 6a8d13b02a50 -r 1002866230b8 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 03 18:59:49 2022 +0900
+++ b/src/zorn.agda	Mon Jul 04 07:41:30 2022 +0900
@@ -289,7 +289,7 @@
       chain : HOD
       chain-uniq : Chain A f mf ay z chain 
 
-record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init)  (zc0 :  ZChain1 A f mf ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) ( z : Ordinal ) (zc0 :  ZChain1 A f mf ay z )  : Set (Level.suc n) where
    chain : HOD
    chain = ZChain1.chain zc0
    field
@@ -365,7 +365,7 @@
      cf-is-≤-monotonic : (nmx : ¬ Maximal A ) →  ≤-monotonic-f A ( cf nmx )
      cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax  ))  , proj2 ( cf-is-<-monotonic nmx x ax  ) ⟫
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A) ) (zc : ZChain A f mf as0 zc0 (& A) ) 
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A) ) (zc : ZChain A f mf as0 (& A) zc0  ) 
         (total : IsTotalOrderSet (ZChain.chain zc) )  → SUP A (ZChain.chain zc)
      sp0 f mf zc0 zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total 
      zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P
@@ -374,7 +374,7 @@
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A)) (zc : ZChain A f mf as0 zc0 (& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A)) (zc : ZChain A f mf as0 (& A) zc0 )
             → (total : IsTotalOrderSet (ZChain.chain zc) )
             → f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc  total))
      fixpoint f mf zc0 zc total = z14 where
@@ -423,7 +423,7 @@
      -- ZChain forces fix point on any ≤-monotonic function (fixpoint)
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
-     z04 :  (nmx : ¬ Maximal A ) → (zc0 : ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 (& A)) (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 zc0 (& A)) 
+     z04 :  (nmx : ¬ Maximal A ) → (zc0 : ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 (& A)) (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) zc0 ) 
            → IsTotalOrderSet (ZChain.chain zc) → ⊥
      z04 nmx zc0 zc total = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1 ))))
                                                (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) )
@@ -477,16 +477,16 @@
           chainq z z<x = ZChain1.chain-uniq ( prev z z<x)
           sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
-          ... | no noax = record { chain = UnionCF A x chainf ; chain-uniq = ? } -- ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ?  } 
+          ... | no noax = record { chain = UnionCF A x chainf ; chain-uniq = ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ? ? } 
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )   
-          ... | case1 pr = record { chain = UnionCF A x chainf  ; chain-uniq = ? } -- ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? } 
+          ... | case1 pr = record { chain = UnionCF A x chainf  ; chain-uniq = ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? ? } 
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax )
           ... | case1 is-sup = ?
           ... | case2 ¬x=sup = ?
 
-     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 :  ZChain1 A f mf ay (& A)) 
-         → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x
-     ind f mf {y} ay x zc0 prev with Oprev-p x
+     ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) 
+         → ((z : Ordinal) → z o< x → (zc1 : ZChain1 A f mf ay z) → ZChain A f mf ay z zc1 ) → (zc0 :  ZChain1 A f mf ay x ) → ZChain A f mf ay x zc0 
+     ind f mf {y} ay x prev zc0 with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
@@ -494,8 +494,8 @@
           px = Oprev.oprev op
           supf : Ordinal → HOD
           supf x = ZChain1.chain zc0 
-          zc : ZChain A f mf ay zc0 (Oprev.oprev op)
-          zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
+          zc : ZChain A f mf ay (Oprev.oprev op) ?
+          zc = ? -- prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) 
           zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
           px<x : px o< x
@@ -505,7 +505,7 @@
           --
           no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
                     HasPrev A (ZChain.chain zc) ab f ∨  IsSup A (ZChain.chain zc) ab →
-                            * a < * b → odef (ZChain.chain zc) b ) → ZChain A f mf ay {!!}  x
+                            * a < * b → odef (ZChain.chain zc) b ) → ZChain A f mf ay x {!!}  
           no-extenion is-max = record { chain⊆A = {!!} -- subst (λ k → k ⊆' A ) {!!} (ZChain.chain⊆A zc)
                      ; initial = subst (λ k →  {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) {!!} (ZChain.initial zc)
                      ; f-next =  subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) {!!} (ZChain.f-next zc) 
@@ -529,7 +529,7 @@
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
-          zc4 : ZChain A f mf ay zc0 x 
+          zc4 : ZChain A f mf ay x zc0 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax = no-extenion zc1  where -- ¬ A ∋ p, just skip
                 zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) →
@@ -662,8 +662,8 @@
                      ; initial = {!!} ; chain∋init  = {!!} ; is-max = {!!} }   where --- limit ordinal case
          supf : Ordinal → HOD
          supf x = ZChain1.chain zc0 
-         uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf ay zc0 (UChain.u u)
-         uzc {z} u =  prev (UChain.u u) (UChain.u<x u) 
+         uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf ay (UChain.u u) ?
+         uzc {z} u =  ? -- prev (UChain.u u) (UChain.u<x u) 
          Uz : HOD
          Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
          u-next : {z : Ordinal} → odef Uz z → odef Uz (f z)
@@ -703,8 +703,8 @@
      SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x
      SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x
 
-     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (SZ0 f mf ay (& A))  (& A)
-     SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay (SZ0 f mf ay (& A))  z  } (λ x → ind f mf ay x (SZ0 f mf ay (& A))  ) (& A)
+     SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) (SZ0 f mf ay (& A))  
+     SZ f mf {y} ay = TransFinite {λ z → (zc1 : ZChain1 A f mf ay z ) → ZChain A f mf ay z zc1  } (λ x zc0 → ind f mf ay x zc0   ) (& A) (SZ0 f mf ay (& A))
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -724,7 +724,7 @@
               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) ) ⟫
          zc0 : (x : Ordinal) → ZChain1 A  (cf nmx) (cf-is-≤-monotonic nmx) as0 x
          zc0 x = TransFinite {λ z → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx)  as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  as0) x
-         zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (zc0 (& A)) (& A)
+         zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) (zc0 (& A)) 
          zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
          total : IsTotalOrderSet (ZChain.chain zorn04)
          total {a} {b} = zorn06  where