# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658827444 -32400
# Node ID 4d9f7d8beedf5bb6278d3428f103e63a1478ac0b
# Parent  c32e85b55e1930f940c7cedfc8440428c28d50da
...

diff -r c32e85b55e19 -r 4d9f7d8beedf src/zorn.agda
--- a/src/zorn.agda	Tue Jul 26 15:14:35 2022 +0900
+++ b/src/zorn.agda	Tue Jul 26 18:24:04 2022 +0900
@@ -265,7 +265,6 @@
 
 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
    field
-      csupz    : FClosure A f (supf u) z 
       fcy<sup  : {z : Ordinal } → FClosure A f y z → (z ≡ supf u) ∨ ( z << supf u ) 
       order    : {sup1 z1 : Ordinal} → (lt : supf sup1 o< supf u ) → FClosure A f (supf sup1 ) z1 → (z1 ≡ supf u ) ∨ ( z1 << supf u )
 
@@ -357,7 +356,7 @@
           ... | case1 eq =  subst (λ k → * b < k ) eq ct00
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct00 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) with trio< (supf ua) (supf ub)
-     ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ (ChainP.csupz supa)
+     ... | tri< a₁ ¬b ¬c with ChainP.order supb  a₁ fca 
      ... | case1 eq with s≤fc (supf ub) f mf fcb 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -374,7 +373,7 @@
           ... | case2 lt =  IsStrictPartialOrder.trans POO ct03 lt
      ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri≈ ¬a  eq ¬c 
          = fcn-cmp (supf ua) f mf fca (subst (λ k → FClosure A f k b ) (sym eq) fcb )
-     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c (ChainP.csupz supb)
+     ct-ind xa xb {a} {b} (ch-is-sup ua supa fca) (ch-is-sup ub supb fcb) | tri> ¬a ¬b c with ChainP.order supa c fcb 
      ... | case1 eq with s≤fc (supf ua) f mf fca 
      ... | case1 eq1 = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym ct00)) lt)) ct00  (λ lt → ⊥-elim (<-irr (case1 ct00) lt)) where
           ct00 : * a ≡ * b
@@ -396,7 +395,7 @@
 
 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 {  fcy<sup = ChainP.fcy<sup cp ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
+ChainP-next A f mf {y} ay supf {x} {z} cp = record {  fcy<sup = ChainP.fcy<sup cp ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -521,8 +520,7 @@
                            → FClosure A f (ZChain.supf zc sup1) z1 → z1 <= ZChain.supf zc b
                     m09 {sup1} {z} s<b fcz = ZChain.order zc b<A s<b fcz
                     m06 : ChainP A f mf ay (ZChain.supf zc) b b
-                    m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) 
-                      ; fcy<sup = m08  ; order = m09 } 
+                    m06 = record {  fcy<sup = m08  ; order = m09 } 
         ... | no lim = record { is-max = is-max }  where
            is-max :  {a : Ordinal} {b : Ordinal} → odef (UnionCF A f mf ay (ZChain.supf zc) x) a →
               b o< x → (ab : odef A b) →
@@ -544,7 +542,7 @@
                  m05 = sym (ZChain.sup=u zc ab m09
                       record { x<sup = λ lt → IsSup.x<sup is-sup (chain-mono2 x (o<→≤ (ob<x lim b<x)) o≤-refl lt )} )   -- ZChain on x
                  m06 : ChainP A f mf ay (ZChain.supf zc) b b
-                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; order = m08 }
+                 m06 = record { fcy<sup = m07 ;  order = m08 }
                  m04 : odef (UnionCF A f mf ay (ZChain.supf zc) (osuc b)) b
                  m04 = ⟪ ab , ch-is-sup b  m06 (subst (λ k → FClosure A f k b) m05 (init ab))  ⟫
 
@@ -663,7 +661,7 @@
                uz04 : {sup1 z1 : Ordinal} → isupf sup1 o< isupf spi → FClosure A f (isupf sup1) z1 → (z1 ≡ isupf spi) ∨ (z1 << isupf spi)
                uz04 {s} {z} s<spi fcz = ⊥-elim ( o<¬≡ refl s<spi )
                uz02 :  ChainP A f mf ay isupf spi (isupf z)
-               uz02 = record { csupz = init asi ; fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
+               uz02 = record { fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
 
 
      --
@@ -763,8 +761,8 @@
           psupf : Ordinal → Ordinal
           psupf z with trio< z x 
           ... | tri< a ¬b ¬c = ZChain.supf (pzc (osuc z) (ob<x lim a)) z
-          ... | tri≈ ¬a b ¬c = spu
-          ... | tri> ¬a ¬b c = spu
+          ... | tri≈ ¬a b ¬c = spu              -- ^^ this z dependcy have to removed
+          ... | tri> ¬a ¬b c = spu   ----  ∀ z o< x , max (supf (pzc (osuc z) (ob<x lim a)))
 
           psupf<z : {z : Ordinal } → ( a : z o< x ) → psupf z ≡ ZChain.supf (pzc (osuc z) (ob<x lim a)) z
           psupf<z {z} z<x with trio< z x
@@ -796,12 +794,14 @@
                       ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
                       zc21 :  {sup1 z1 : Ordinal} → psupf sup1 o< psupf z → FClosure A f (psupf sup1) z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
                       zc21 {s} {z1} s<z fc = zc22 where
+                        zc25 : psupf z ≡ ZChain.supf ozc z 
+                        zc25 = psupf<z z<x
+                        s<x : s o< x
+                        s<x = ?
+                        zc26 : psupf s ≡ ZChain.supf (pzc (osuc s) (ob<x lim s<x))  s 
+                        zc26 = psupf<z s<x
                         zc23 : ZChain.supf ozc s o< ZChain.supf ozc z
-                        zc23 with trio< s x
-                        ... | tri< a ¬b ¬c = subst₂ (λ j k → j o< k ) 
-                            (cong (λ k → ZChain.supf (pzc (osuc z) (ob<x lim k)) _ ) o<-irr) (psupf<z z<x)  s<z
-                        ... | tri≈ ¬a b ¬c = ?
-                        ... | tri> ¬a ¬b c = ?
+                        zc23 = ?
                         zc24 : FClosure A f (ZChain.supf ozc s) z1
                         zc24 with trio< s x
                         ... | t = ?
@@ -810,8 +810,7 @@
                         ... | case1 eq = case1 (trans eq (sym eq1) )
                         ... | case2 lt = case2 (subst ( λ k → z1 << k ) (sym eq1) lt)
                       cp1 : ChainP A f mf ay psupf z (ZChain.supf ozc z)
-                      cp1 = record { csupz =  (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) 
-                           ; fcy<sup = zc20   ; order = zc21 }
+                      cp1 = record {  fcy<sup = zc20   ; order = zc21 }
 
                      ---  u = supf u = supf z 
           ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? ? ? ⟫ where