# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1656842389 -32400
# Node ID 6a8d13b02a508e5d38259077062931f63088e5c9
# Parent  5f85e71b2490c17da04bc2abd7d03273804deb1b
...

diff -r 5f85e71b2490 -r 6a8d13b02a50 src/zorn.agda
--- a/src/zorn.agda	Sun Jul 03 17:08:55 2022 +0900
+++ b/src/zorn.agda	Sun Jul 03 18:59:49 2022 +0900
@@ -253,44 +253,45 @@
 UnionCF : (A : HOD) (x : Ordinal) (chainf : (z : Ordinal ) → z o< x → HOD ) → HOD
 UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
 
-data Chain (A : HOD ) ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) : Ordinal →  HOD  → Set (Level.suc n) where
-    ch-noax    : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f ay (Oprev.oprev op) chain) → Chain A f ay x chain
+data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) : Ordinal →  HOD  → Set (Level.suc n) where
+    ch-init    : Chain A f mf  ay o∅  record { od = record { def = λ z → FClosure A f y z  } ; odmax = & A ; <odmax = λ {y} sy → ? }
+    ch-noax    : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f mf  ay (Oprev.oprev op) chain) → Chain A f mf  ay x chain
     ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) 
-        ( c : Chain A f ay (Oprev.oprev op) chain) ( h :  HasPrev A chain ax f ) → Chain A f ay x chain
+        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( h :  HasPrev A chain ax f ) → Chain A f mf ay x chain
     ch-is-sup : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
-        ( c : Chain A f ay (Oprev.oprev op) chain) ( nh :  ¬ HasPrev A chain  ax f ) ( sup : IsSup A chain   ax ) → Chain A f ay x 
+        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( nh :  ¬ HasPrev A chain  ax f ) ( sup : IsSup A chain   ax ) → Chain A f mf ay x 
             record { od = record { def = λ z → odef A z ∧ (odef chain z ∨ (FClosure A f x z)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
     ch-skip : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) ( ax : odef A x ) 
-        ( c : Chain A f ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f ay x chain
+        ( c : Chain A f mf ay (Oprev.oprev op) chain) ( nh : ¬  HasPrev A chain ax f ) ( nsup : ¬ IsSup A chain ax ) → Chain A f mf ay x chain
     ch-noax-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( noax : ¬ odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
-         → Chain A f ay x (UnionCF A x chainf )
+         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
+         → Chain A f mf ay x (UnionCF A x chainf )
     ch-hasprev-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
+         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
          → ( h :   HasPrev A (UnionCF A x chainf)  ax f ) 
-         → Chain A f ay x (UnionCF A x chainf )
+         → Chain A f mf ay x (UnionCF A x chainf )
     ch-is-sup-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
+         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
          →  ( nh :  ¬ HasPrev A (UnionCF A x chainf) ax f ) ( sup : IsSup A (UnionCF A x chainf) ax ) 
-         → Chain A f ay x 
-             record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f y x ) } 
+         → Chain A f mf ay x 
+             record { od = record { def = λ z → odef A z ∧ (UChain x chainf z ∨ FClosure A f x z ) } 
                 ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
     ch-skip-union : {x : Ordinal } { chain : HOD } ( nop : ¬ Oprev Ordinal osuc x ) ( ax : odef A x ) 
-         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f ay z ( chainf z z<x ))
+         → ( chainf : ( z : Ordinal ) → z o< x → HOD ) → ( lt : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ))
          →  (nh : ¬ HasPrev A (UnionCF A x chainf) ax f ) (nsup :  ¬ IsSup A (UnionCF A x chainf) ax ) 
-         → Chain A f ay x (UnionCF A x chainf) 
+         → Chain A f mf ay x (UnionCF A x chainf) 
 
-ChainF : (A : HOD) →  ( f : Ordinal → Ordinal ) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f ay (& A) chain → (x : Ordinal) → x o< & A →  HOD
-ChainF A f {y} ay chain Ch x x<a = {!!}
+ChainF : (A : HOD) →  ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → (chain : HOD ) → Chain A f mf ay (& A) chain → (x : Ordinal) → x o< & A →  HOD
+ChainF A f mf {y} ay chain Ch x x<a = {!!}
 
-record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal ) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
+record ZChain1 ( A : HOD )    ( f : Ordinal → Ordinal )  (mf : ≤-monotonic-f A f) {y : Ordinal } (ay : odef A y ) ( z : Ordinal ) : Set (Level.suc n) where
    field
       chain : HOD
-      chain-uniq : Chain A f ay z chain 
+      chain-uniq : Chain A f mf ay z chain 
 
-record ZChain ( A : HOD )    ( f : Ordinal → Ordinal ) {init : Ordinal} (ay : odef A init)  (zc0 :  ZChain1 A f 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)  (zc0 :  ZChain1 A f mf ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where
    chain : HOD
-   chain = {!!}
+   chain = ZChain1.chain zc0
    field
       chain⊆A : chain ⊆' A
       chain∋init : odef chain init
@@ -364,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 as0 (& A) ) (zc : ZChain A f 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 zc0 (& A) ) 
         (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
@@ -373,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 as0 (& A)) (zc : ZChain A f 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 zc0 (& A) )
             → (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
@@ -422,7 +423,8 @@
      -- 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) as0 (& A)) (zc : ZChain A (cf nmx) as0 zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥
+     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)) 
+           → 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) )
            (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc0 zc total ))) -- x ≡ f x ̄
@@ -436,16 +438,16 @@
      --
 
      sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal)
-         → ((z : Ordinal) → z o< x → ZChain1 A f ay z ) → ZChain1 A f ay x
+         → ((z : Ordinal) → z o< x → ZChain1 A f mf ay z ) → ZChain1 A f mf ay x
      sind f mf {y} ay x prev  with Oprev-p x
      ... | yes op = sc4 where
           open ZChain1
           px = Oprev.oprev op
           px<x : px o< x
           px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc 
-          sc : ZChain1 A f ay px
+          sc : ZChain1 A f mf ay px
           sc = prev px px<x
-          sc4 : ZChain1 A f ay x
+          sc4 : ZChain1 A f mf ay x
           sc4 with ODC.∋-p O A (* x)
           ... | no noax = record { chain = chain sc ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc )  } 
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc ) ax f )   
@@ -460,7 +462,7 @@
                     ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy }
                 sc7 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f
                 sc7 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
-                sc9 : Chain A f ay x schain
+                sc9 : Chain A f mf ay x schain
                 sc9 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc7
                     record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-sup lt) }
           ... | case2 ¬x=sup = record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } where
@@ -468,10 +470,12 @@
                 sc17 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) }
                 sc10 : ¬ IsSup A (chain sc) (subst (λ k → odef A k) &iso ax)
                 sc10 not = ¬x=sup ( record { x<sup  = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) }  )
-     ... | no ¬ox = {!!} where
+     ... | no ¬ox = sc4 where
           chainf : (z : Ordinal) → z o< x → HOD
           chainf z z<x = ZChain1.chain ( prev z z<x )
-          sc4 : ZChain1 A f ay x
+          chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x )
+          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) ?  } 
           ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f )   
@@ -480,8 +484,8 @@
           ... | 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 ay (& A)) 
-         → ((z : Ordinal) → z o< x → ZChain A f ay zc0 z) → ZChain A f ay zc0 x
+     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
      ... | yes op = zc4 where
           --
@@ -490,7 +494,7 @@
           px = Oprev.oprev op
           supf : Ordinal → HOD
           supf x = ZChain1.chain zc0 
-          zc : ZChain A f ay zc0 (Oprev.oprev op)
+          zc : ZChain A f mf ay zc0 (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 
@@ -501,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 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) 
@@ -525,7 +529,7 @@
                 ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a  b<x )
                 ... | tri> ¬a ¬b c  = ⊥-elim (¬a  b<x )
 
-          zc4 : ZChain A f ay zc0 x 
+          zc4 : ZChain A f mf ay zc0 x 
           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) →
@@ -658,7 +662,7 @@
                      ; 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 ay zc0 (UChain.u u)
+         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) 
          Uz : HOD
          Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!}  }
@@ -696,11 +700,11 @@
          ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z
          ... | case2 z<y  = ordtrans x<z z<y
          
-     SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f ay x
-     SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f ay z} (sind f mf ay ) x
+     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 ay (SZ0 f mf ay (& A))  (& A)
-     SZ f mf {y} ay = TransFinite {λ z → ZChain A f 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 (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)
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
@@ -718,9 +722,9 @@
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where
               zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) →  odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) 
               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) as0 x
-         zc0 x = TransFinite {λ z → ZChain1 A (cf nmx) as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx)  as0) x
-         zorn04 : ZChain A (cf nmx) as0 (zc0 (& A)) (& A)
+         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 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) 
          total : IsTotalOrderSet (ZChain.chain zorn04)
          total {a} {b} = zorn06  where