# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1654594677 -32400
# Node ID 9922bfe92278ff99c5aba51abb24c77b26ed8293
# Parent  b684030c8a28c3f65babeef35346a2b11f980bb9
ZChain∧Chain

diff -r b684030c8a28 -r 9922bfe92278 src/zorn.agda
--- a/src/zorn.agda	Tue Jun 07 18:01:28 2022 +0900
+++ b/src/zorn.agda	Tue Jun 07 18:37:57 2022 +0900
@@ -89,9 +89,6 @@
 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
 
--- immieate-f : (A : HOD) → ( f : Ordinal → Ordinal )  → Set n
--- immieate-f A f = { x y : Ordinal } → odef A x → odef A y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
-
 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
    init : odef A s → FClosure A f s s
    fsuc : (x : Ordinal) ( p :  FClosure A f s x ) → FClosure A f s (f x)
@@ -235,11 +232,10 @@
    field
       x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x )
 
-record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) (Chain : HOD)
+record ZChain ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal ) 
                   ( z : Ordinal ) : Set (Level.suc n) where
-   chain : HOD
-   chain = Chain
    field
+      chain : HOD
       chain⊆A : chain ⊆' A
       chain∋x : odef chain x
       initial : {y : Ordinal } → odef chain y → * x ≤ * y
@@ -251,6 +247,14 @@
           → * a < * b  → odef chain b
       fc∨sup :  {a : Ordinal } → ( ca : odef chain a ) → HasPrev A chain ( chain⊆A ca) f  ∨ IsSup A chain  ( chain⊆A ca)
 
+record ZChain∧Chain  ( A : HOD )  (x : Ordinal)  ( f : Ordinal → Ordinal )
+                  ( z : Ordinal ) : Set (Level.suc n) where
+   field
+      zchain : ZChain A x f z
+      chainf :  (b : Ordinal) → HOD
+      chain-mono :  {a b : Ordinal} → a o< b → chainf a  ⊆' chainf b
+      chain=zchain : {b : Ordinal} → chainf z ≡ ZChain.chain zchain 
+      
 record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
@@ -273,10 +277,6 @@
 Zorn-lemma {A}  0<A supP = zorn00 where
      supO : (C : HOD ) → C ⊆' A → IsTotalOrderSet C → Ordinal
      supO C C⊆A TC = & ( SUP.sup ( supP  C  C⊆A TC ))
-     postulate
-        --- irrelevance of ⊆' and compare
-        sup== : {C C1 : HOD } → C ≡ C1 → {c  : C ⊆' A } {c1 : C1 ⊆' A } → {t  : IsTotalOrderSet C } {t1 : IsTotalOrderSet C1 }
-         → SUP.sup ( supP  C c t )  ≡  SUP.sup ( supP  C1 c1 t1 )
      <-irr0 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      <-irr0 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
@@ -320,20 +320,12 @@
      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  ) ⟫
 
-     cind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
-            ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A y f (Chain z) z ) → { y : Ordinal } → (ya : odef A y) → HOD
-     cind = ?
-
-     Chain : (x : Ordinal) → HOD
-     Chain = {!!}
-
-     ind f mf x prev {y} ay with Oprev-p x
-     zsup :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) →  (zc : ZChain A (& s) f (Chain (& A)) (& A) ) → SUP A  (ZChain.chain zc) 
+     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  )   
-     A∋zsup :  (nmx : ¬ Maximal A ) (zc : ZChain A (& s) (cf nmx) (Chain (& A)) (& A) ) 
+     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 (Chain (& A))(& A) ) → SUP A (ZChain.chain 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) 
      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)
@@ -341,7 +333,7 @@
      ---
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
-     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (Chain (& A))(& A) )
+     fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) )
             → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
      fixpoint f mf zc = z14 where
            chain = ZChain.chain zc
@@ -389,7 +381,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 ) → (zc : ZChain A (& s) (cf nmx) (Chain (& A)) (& A)) → ⊥
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx)  (& A)) → ⊥
      z04 nmx zc = <-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 ) zc ))) -- x ≡ f x ̄
@@ -397,26 +389,31 @@
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
 
+     ind1 :   ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) →  (x : Ordinal)
+          → ((y : Ordinal) → y o< x → {y = y₁ : Ordinal} → odef A y₁ → ZChain∧Chain A y₁ f y) →
+            {y : Ordinal} → odef A y → ZChain∧Chain A y f x
+     ind1 = {!!}
+
      --
      -- create all ZChains under o< x
      --
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
-            ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A y f (Chain z) z ) → { y : Ordinal } → (ya : odef A y) → ZChain A y f (Chain x) x
+            ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A y f z ) → { y : Ordinal } → (ya : odef A y) → ZChain A y f x
      ind f mf x prev {y} ay with Oprev-p x
      ... | yes op = zc4 where
           --
           -- we have previous ordinal to use induction
           --
           px = Oprev.oprev op
-          zc0 : ZChain A y f (Chain (Oprev.oprev op)) (Oprev.oprev op)
+          zc0 : ZChain A y f (Oprev.oprev op)
           zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ay
           zc0-b<x : (b : Ordinal ) → b o< x → b o< osuc px
           zc0-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt 
 
-          zc4 : ZChain A y f (Chain x) x 
+          zc4 : ZChain A y f x 
           zc4 with ODC.∋-p O A (* x)
           ... | no noax =  -- ¬ A ∋ p, just skip
-                 record {  chain⊆A = ZChain.chain⊆A zc0 ; initial = ZChain.initial zc0 
+                 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-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc11 ; fc∨sup = {!!} }  where -- no extention
                 zc11 : {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -434,13 +431,13 @@
                 zc17 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox
                 ... | case2 lt = ZChain.is-max zc0 za (zc0-b<x b lt) ab P a<b
                 ... | case1 b=x = subst (λ k → odef chain k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc0 (HasPrev.ay pr))
-                zc9 :  ZChain A y f (Chain x) x
-                zc9 = record {  chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next =  ZChain.f-next zc0 -- no extention
+                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
                      ; initial = ZChain.initial zc0 ; f-immediate =  ZChain.f-immediate zc0 ; chain∋x  = ZChain.chain∋x zc0 ; is-max = zc17 ; fc∨sup = {!!}}  
           ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc0) ax )
           ... | case1 is-sup = -- x is a sup of zc0 
-                record { chain⊆A = {!!} ; f-total = {!!} ; f-next = {!!} 
-                     ; initial = {!!} ; f-immediate =  {!!} ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = {!!} ; fc∨sup = {!!}} where 
+                record { chain = schain ; chain⊆A = s⊆A  ; f-total = scmp ; f-next = scnext 
+                     ; initial = scinit ; f-immediate =  simm ; chain∋x  = case1 (ZChain.chain∋x zc0) ; is-max = s-ismax ; fc∨sup = {!!}} where 
                 sup0 : SUP A (ZChain.chain zc0) 
                 sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where
                         x21 :  {y : HOD} → ZChain.chain zc0 ∋ y → (y ≡ * x) ∨ (y < * x)
@@ -540,7 +537,7 @@
                      ... | case1 y=b  = subst (λ k → odef chain 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 sup of former ZChain from y
-                   record {  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-total = ZChain.f-total 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 ; fc∨sup = {!!} }  where
                       -- no extention
                 z18 :  {a b : Ordinal} → odef (ZChain.chain zc0) a → b o< osuc x → (ab : odef A b) →
@@ -553,13 +550,13 @@
                 ... | 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 with trio< x y
-     ... | tri< a ¬b ¬c = record { chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!}
+     ... | tri< a ¬b ¬c = record { chain = {!!} ; chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!}
                      ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }
      ... | tri≈ ¬a b ¬c = {!!}
      ... | tri> ¬a ¬b y<x = {!!} where
-       UnionZ : ZChain A y f (Chain x) x
-       UnionZ = record {  chain⊆A = {!!}  ; f-total = {!!}  ; f-next = {!!}
-                     ; initial = {!!} ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
+       UnionZ : ZChain A y f x
+       UnionZ = record { chain = Uz ; chain⊆A = Uz⊆A  ; f-total = u-total  ; f-next = u-next
+                     ; initial = u-initial ; f-immediate = {!!} ; chain∋x  = {!!} ; is-max = {!!} ; fc∨sup = {!!} }  where --- limit ordinal case
          record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x
             field
                u : Ordinal
@@ -567,7 +564,7 @@
                chain∋z : odef (ZChain.chain (prev u u<x {y} ay )) z
          Uz⊆A : {z : Ordinal} → UZFChain z → odef A z
          Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) {y} ay ) (UZFChain.chain∋z u)
-         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (Chain (UZFChain.u u)) (UZFChain.u u)
+         uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u)
          uzc {z} u =  prev (UZFChain.u u) (UZFChain.u<x u) {y} ay
          Uz : HOD
          Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A
@@ -598,11 +595,14 @@
          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) ) ⟫
-         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (Chain (& A)) (& A)
-         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f (Chain z) z } (ind f mf) (& A)
-         zorn04 : ZChain A (& s) (cf nmx) (Chain (& A))   (& A)
+         zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A (& s) f (& A)
+         zorn03 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain A y f z } (ind f mf) (& A)
+         zorn04 : ZChain A (& s) (cf nmx)  (& A)
          zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )
 
+         zorn05 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain∧Chain A (& s) f (& A)
+         zorn05 f mf = TransFinite {λ z → {y : Ordinal } → (ya : odef A y ) → ZChain∧Chain  A y f z } {!!} (& A)
+
 -- usage (see filter.agda )
 --
 -- _⊆'_ : ( A B : HOD ) → Set n