# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1658813513 -32400
# Node ID 6a48f8eb8b53f699f69bf541ca436f6189c3277c
# Parent  068cba4ee934744687dc0e19c061d0096e569d3c
...

diff -r 068cba4ee934 -r 6a48f8eb8b53 src/zorn.agda
--- a/src/zorn.agda	Tue Jul 26 10:07:42 2022 +0900
+++ b/src/zorn.agda	Tue Jul 26 14:31:53 2022 +0900
@@ -266,7 +266,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 
-      supfu=u  : supf u ≡ u 
       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 )
 
@@ -397,8 +396,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 { supfu=u  = ChainP.supfu=u cp  
-     ; 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 ; csupz = fsuc _ (ChainP.csupz cp) ; order = ChainP.order cp }
 
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
@@ -523,7 +521,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) ; supfu=u = sym m05 
+                    m06 = record { csupz = subst (λ k → FClosure A f k b) m05 (init ab) 
                       ; 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 →
@@ -546,8 +544,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
-                       ; supfu=u = sym m05 }
+                 m06 = record { fcy<sup = m07 ; csupz = subst (λ k →  FClosure A f k b ) m05 (init ab) ; 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))  ⟫
 
@@ -666,7 +663,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 ; supfu=u = refl ; fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
+               uz02 = record { csupz = init asi ; fcy<sup = uz03 ; order = λ {s} {z} → uz04 {s} {z} }
 
 
      --
@@ -787,44 +784,26 @@
           csupf z with trio< z x | inspect psupf z
           ... | tri< z<x ¬b ¬c | record { eq = eq1 } = zc11 where
                 ozc = pzc (osuc z) (ob<x lim z<x)
-                oz<x : osuc z o< x
-                oz<x = ?
                 zc12 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc z)
                 zc12  = ZChain.csupf ozc z
                 zc11 : odef A (ZChain.supf ozc z) ∧ UChain A f mf ay psupf x (ZChain.supf ozc z)
-                zc11 with ZChain.csupf ozc z | inspect (ZChain.csupf ozc) z
-                ... | ⟪ az , ch-init fc ⟫ | _ = ⟪ az , ch-init fc ⟫ 
-                ... | ⟪ az , ch-is-sup u is-sup fc ⟫ | record { eq = eq2 } 
-                   = ⟪ az , ch-is-sup u zc18 (subst (λ k → FClosure A f k _) zc16 fc)  ⟫  where
-                      zc14 : ZChain.csupf ozc z ≡ ⟪ az , ch-is-sup u is-sup fc ⟫
-                      zc14 = eq2
-                      zc13 : odef A (ZChain.supf ozc u) ∧ UChain A f mf ay (ZChain.supf ozc) (osuc z) (ZChain.supf ozc u)
-                      zc13  = ZChain.csupf ozc u
-                      zc15 : FClosure A f (ZChain.supf ozc u) (ZChain.supf ozc z) 
-                      zc15 = fc
-                      zc17 : u ≡ psupf z
-                      zc17 = ?
-                      zc19 : u o< x
-                      zc19 = ?
-                      zc16 : ZChain.supf ozc u ≡ psupf u 
-                      zc16 = ?
-                      zc18 : ChainP A f mf ay psupf u (ZChain.supf ozc z)
-                      zc18 = record { csupz = subst (λ k → FClosure A f k _) zc16 fc
-                         ; supfu=u = ? ; fcy<sup = ? ; order = ? }
-          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup spu zc15 
-                  (subst (λ k → FClosure A f k spu) zc18 (init sa))  ⟫ where
+                zc11 = ⟪ az , ch-is-sup z cp1 (subst (λ k → FClosure A f k _) (sym eq1) (init az) ) ⟫ where
+                      az : odef A ( ZChain.supf ozc z )
+                      az = proj1 zc12
+                      zc20 : {z1  : Ordinal} → FClosure A f y z1 → (z1 ≡ psupf z) ∨ (z1 << psupf z)
+                      zc20 {z1} fc with ZChain.fcy<sup ozc <-osuc fc
+                      ... | case1 eq = case1 (trans eq (sym eq1) )
+                      ... | 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 = ?
+                      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 }
+
+                     ---  u = supf u = supf z 
+          ... | tri≈ ¬a b ¬c | record { eq = eq1 } = ⟪ sa , ch-is-sup ? ? ? ⟫ where
                 sa = SUP.A∋maximal usup
-                zc18 : spu ≡ psupf spu
-                zc18 = ?
-                zc17 : spu ≡ psupf x 
-                zc17 = subst (λ k → spu ≡ psupf k  ) b (sym eq1) 
-                zc15 : ChainP A f mf ay psupf spu spu
-                zc15 = record { csupz = subst (λ k → FClosure A f k spu) zc18 (init sa)
-                         ; supfu=u = sym zc18 ; fcy<sup = ? ; order = ? }
-          ... | tri> ¬a ¬b c | record { eq = eq1 } = ⟪ SUP.A∋maximal usup , ch-is-sup x zc16
-                  (subst (λ k → FClosure A f k spu) psupf=x (init (SUP.A∋maximal usup)))  ⟫ where
-                zc16 : ChainP A f mf ay psupf x spu
-                zc16 = ?
+          ... | tri> ¬a ¬b c | record { eq = eq1 } = ?
 
           pchain : HOD
           pchain = UnionCF A f mf ay psupf x