# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658162067 -32400
# Node ID 2c0fe13e3e5c6ac1f0831cbeb476858b25590afd
# Parent  ac6b4d200f27588920accb2a8ac615de0df8abe4
x in ChainP

diff -r ac6b4d200f27 -r 2c0fe13e3e5c src/zorn.agda
--- a/src/zorn.agda	Tue Jul 19 01:15:05 2022 +0900
+++ b/src/zorn.agda	Tue Jul 19 01:34:27 2022 +0900
@@ -262,8 +262,9 @@
 --    minimum index is y not ϕ 
 --
 
-record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (u z : Ordinal) : Set n where
+record ChainP (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) (x u z : Ordinal) : Set n where
    field
+      u≤x      : u o≤ x
       u>0      : o∅ o< u    -- ¬ ch-init
       au       : odef A u
       ¬u=fx    : {x : Ordinal} → ¬ ( u ≡ f x )
@@ -272,11 +273,11 @@
       csupz    : FClosure A f (supf u) z 
       order    : {sup1 z1 : Ordinal} → (lt : sup1 o< u ) → FClosure A f (supf sup1 ) z1 → z1 << supf u
 
-data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) : Ordinal →  Ordinal → Set n where
-    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf o∅ z 
+data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal) x : Ordinal →  Ordinal → Set n where
+    ch-init    : (z : Ordinal) → FClosure A f y z  → Chain A f mf  ay supf x o∅ z 
     ch-is-sup : {sup z : Ordinal } 
-         → ( is-sup : ChainP A f mf ay supf sup z)
-         → ( fc : FClosure A f (supf sup) z ) → Chain A f mf ay supf sup z
+         → ( is-sup : ChainP A f mf ay supf x sup z)
+         → ( fc : FClosure A f (supf sup) z ) → Chain A f mf ay supf x sup z
 
 -- Union of supf z which o< x
 --
@@ -286,7 +287,7 @@
    field
       u : Ordinal
       u<x : (u o< x ) ∨ ( u ≡ o∅)
-      uchain : Chain A f mf ay supf u z
+      uchain : Chain A f mf ay supf x u z
 
 ∈∧P→o< :  {A : HOD } {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
 ∈∧P→o< {A } {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
@@ -329,9 +330,9 @@
 -- data Chain is total
 
 chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
-   {s s1 a b : Ordinal } ( ca : Chain A f mf ay supf s a ) ( cb : Chain A f mf ay supf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
-chain-total A f mf {y} ay supf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
-     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay supf xa a → Chain A f mf ay supf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
+   (x : Ordinal) {s s1 a b : Ordinal } ( ca : Chain A f mf ay supf x s a ) ( cb : Chain A f mf ay supf x s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a )
+chain-total A f mf {y} ay supf x {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where
+     ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay supf x xa a → Chain A f mf ay supf x xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a)
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb
      ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01  (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt)  where
           ct00 : * a < * (supf xb)
@@ -365,8 +366,8 @@
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct05 lt
 
 ChainP-next : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
-   → {x z : Ordinal } →  ChainP A f mf ay supf x z → ChainP A f mf ay supf x (f z )
-ChainP-next A f mf {y} ay supf {x} {z} cp = {!!} --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
+   → (x : Ordinal) {u z : Ordinal } →  ChainP A f mf ay supf x u z → ChainP A f mf ay supf x u (f z )
+ChainP-next A f mf {y} ay supf x {u} {z} cp = {!!} --record { y-init = ChainP.y-init cp ; asup = ChainP.asup cp  ; au = ChainP.au cp
      -- ; fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
@@ -440,10 +441,9 @@
            bchain {b} b<x ⟪ ab , record { u = u ; u<x = u=0 ; uchain = ch-init b fc } ⟫ = 
                   ⟪ ab , record { u = u ; u<x = case2 refl ; uchain = ch-init b fc } ⟫ 
            bchain {b} b<x ⟪ ab , record { u = u ; u<x = u<x ; uchain = ch-is-sup is-sup fc } ⟫ =  
-                  ⟪ ab , record { u = u ; u<x = case1 (b01 fc) ; uchain = ch-is-sup is-sup fc } ⟫ where
-               b01 : {b : Ordinal } → FClosure A f (ZChain.supf zc u) b → u o< x
-               b01 (init as) = ?
-               b01 (fsuc z fc) = b01 fc
+                  ⟪ ab , record { u = u ; u<x = case1 (b01 fc) ; uchain = ch-is-sup ? fc } ⟫ where
+               b01 : u o≤ b → u o< x
+               b01 = ?
            chain-mono2 :  {a b c : Ordinal} → a o≤ b → b o≤ x →
                 odef (UnionCF A f mf ay (ZChain.supf zc) a) c → odef (UnionCF A f mf ay (ZChain.supf zc) b) c
            chain-mono2 {a} {b} {c} a≤b b≤x uac = ?
@@ -553,7 +553,7 @@
           itotal : IsTotalOrderSet (UnionCF A f mf ay isupf o∅) 
           itotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay isupf (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
+               uz01 = chain-total A f mf ay isupf o∅ (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
           imax : {a b : Ordinal} → odef (UnionCF A f mf ay isupf o∅) a →
             b o< o∅ → (ab : odef A b) →
             HasPrev A (UnionCF A f mf ay isupf o∅) ab f ∨ IsSup A (UnionCF A f mf ay isupf o∅) ab →
@@ -585,17 +585,17 @@
           ptotal : IsTotalOrderSet pchain
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay (ZChain.supf zc) (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
+               uz01 = chain-total A f mf ay (ZChain.supf zc) x (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
           pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
           pchain⊆A {y} ny = proj1 ny
           pnext : {a : Ordinal} → odef pchain a → odef pchain (f a)
           pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; uchain = fua } ⟫ where
                afa : odef A ( f a )
                afa = proj2 ( mf a aa )
-               fua : Chain A f mf ay (ZChain.supf zc)  (UChain.u ua) (f a)
+               fua : Chain A f mf ay (ZChain.supf zc) x (UChain.u ua) (f a)
                fua with UChain.uchain ua
                ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
+               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ x is-sup ) (fsuc _ fc )
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with UChain.uchain ua
           ... | ch-init a fc = s≤fc y f mf fc
@@ -612,7 +612,7 @@
               ;  chain⊆A = pchain⊆A ;  f-next = pnext ;  f-total = ptotal }
 
           chain-mono : UnionCF A f mf ay (ZChain.supf zc) (Oprev.oprev op ) ⊆' pchain
-          chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = zc11 ; uchain = UChain.uchain (proj2 za)  }  ⟫ where
+          chain-mono {a} za = ⟪ proj1 za , record { u = UChain.u (proj2 za)  ; u<x = zc11 ; uchain = ?  }  ⟫ where
               zc11 : (UChain.u (proj2 za) o< x) ∨ (UChain.u (proj2 za) ≡ o∅)
               zc11 with UChain.u<x (proj2 za)
               ... | case1 z<x = case1 (ordtrans z<x px<x )
@@ -624,13 +624,13 @@
 
           chain-x : ( {z : Ordinal} → (az : odef pchain z) → ¬ ( UChain.u (proj2 az) ≡ px  )) → pchain ⊆' UnionCF A f mf ay (ZChain.supf zc) px
           chain-x ne {z} ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ = 
-              ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = uc } ⟫ 
+              ⟪ az , record { u = u ; u<x = case2 u=y ; uchain = ? } ⟫ 
           chain-x ne {z} ⟪ az , record { u = u ; u<x = case1 u<x ; uchain = ch-init z fc } ⟫ with trio<  o∅ px
           ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-init z fc } ⟫  
           ... | tri≈ ¬a b ¬c = ⟪ az , record { u = u ; u<x = case2 refl ; uchain = ch-init z fc } ⟫  
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
           chain-x ne {z} uz@record { proj1 = az ; proj2 =  record { u = u ; u<x = case1 u<x ; uchain = ch-is-sup is-sup fc } } with trio< u px
-          ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup is-sup fc } ⟫ 
+          ... | tri< a ¬b ¬c = ⟪ az , record { u = u ; u<x = case1 a ; uchain = ch-is-sup ? fc } ⟫ 
           ... | tri≈ ¬a b ¬c = ⊥-elim ( ne uz  b )
           ... | tri> ¬a ¬b c = ⊥-elim ( ¬p<x<op ⟪ c , subst (λ k → u o< k ) (sym (Oprev.oprev=x op))  u<x  ⟫ )
 
@@ -669,7 +669,7 @@
           ptotal : IsTotalOrderSet pchain
           ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
                uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) )
-               uz01 = chain-total A f mf ay psupf0 (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
+               uz01 = chain-total A f mf ay psupf0 x (UChain.uchain (proj2 ca)) (UChain.uchain (proj2 cb)) 
 
           pchain⊆A : {y : Ordinal} → odef pchain y →  odef A y
           pchain⊆A {y} ny = proj1 ny
@@ -677,10 +677,10 @@
           pnext {a} ⟪ aa , ua ⟫ = ⟪ afa , record { u = UChain.u ua ; u<x = UChain.u<x ua ; uchain = fua } ⟫ where
                afa : odef A ( f a )
                afa = proj2 ( mf a aa )
-               fua : Chain A f mf ay psupf0 (UChain.u ua) (f a)
+               fua : Chain A f mf ay psupf0 x (UChain.u ua) (f a)
                fua with UChain.uchain ua
                ... | ch-init a fc = ch-init (f a) ( fsuc _ fc )
-               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ is-sup ) (fsuc _ fc )
+               ... | ch-is-sup is-sup fc = ch-is-sup (ChainP-next A f mf ay _ x is-sup ) (fsuc _ fc )
           pinit :  {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁
           pinit {a} ⟪ aa , ua ⟫  with UChain.uchain ua
           ... | ch-init a fc = s≤fc y f mf fc