# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1666136502 -32400
# Node ID 85f6238a38db2bb75e6c4b7274f6a33e487e70cf
# Parent  620c2f3440f5dc3e3152cdb6ee92a0226a5a2b94
use supf of zchain for (nmx : ¬ Maximal A ) → ⊥

diff -r 620c2f3440f5 -r 85f6238a38db src/zorn.agda
--- a/src/zorn.agda	Mon Oct 17 11:29:37 2022 +0900
+++ b/src/zorn.agda	Wed Oct 19 08:41:42 2022 +0900
@@ -1300,40 +1300,45 @@
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x
      SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z  } (λ x → ind f mf ay x   ) x
 
-     record ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) (z : Ordinal) : Set n where
-       field
-          uz : Ordinal
-          zc : odef (ZChain.chain (SZ f mf ay uz)) z
+     data ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y) 
+            ( supf : Ordinal → Ordinal )  (z : Ordinal) : Set n where
+          zchain : (uz : Ordinal ) → odef (UnionCF A f mf ay supf uz) z → ZChainP f mf ay supf z
 
-     UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  → HOD
-     UnionZF f mf {y} ay = record { od = record { def = λ x → ZChainP f mf ay x } ; odmax = & A ; <odmax = λ lt →  ∈∧P→o< ( ZChainP.zc lt) }
+     UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
+            (supf : Ordinal → Ordinal )  → HOD
+     UnionZF f mf {y} ay supf = record { od = record { def = λ x → ZChainP f mf ay supf x } 
+         ; odmax = & A ; <odmax = λ lt →  ∈∧P→o< ? }
      
-     uztotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  → 
-         IsTotalOrderSet (UnionZF f mf ay)
-     uztotal f mf ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where 
+     uztotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)  {y : Ordinal} (ay : odef A y)  
+         → ( supf : Ordinal → Ordinal )
+         → IsTotalOrderSet (UnionZF f mf ay supf )
+     uztotal f mf ay sz {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 = ?
 
-     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  → SUP A (UnionZF f mf ay )
+     sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
+         → ( supf : Ordinal → Ordinal )
+         → SUP A (UnionZF f mf ay supf )
      -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay)
-     sp0 f mf {x} ay = ? -- supP ? ? ?
+     sp0 f mf {x} ay supf  = supP (UnionZF f mf ay supf ) (λ lt → ? ) (uztotal f mf ay supf )
 
      sp00 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y)  
-         (zc : ZChain A f mf ay x ) → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
-     sp00 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where
+         → (zc : ZChain A f mf ay x ) 
+         → SUP A (UnionCF A f mf ay (ZChain.supf zc) x)
+     sp00 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where
         ztotal : IsTotalOrderSet (ZChain.chain zc) 
         ztotal {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) ( (proj2 ca)) ( (proj2 cb)) 
 
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  
-            → f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 ))
+            → f (& (SUP.sup (sp0 f mf as0 ? ))) ≡ & (SUP.sup (sp0 f mf as0 ? ))
      fixpoint f mf = z14 where
-           chain = UnionZF f mf as0 
+           chain = UnionZF f mf as0 ?
            supf : Ordinal → Ordinal 
            supf = ?
            sp1 : SUP A ?
-           sp1 = sp0 f mf as0 
+           sp1 = sp0 f mf as0 ?
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) 
               →  HasPrev A chain b f ∨  IsSup A chain {b} ab 
               → * a < * b  → odef chain b
@@ -1359,7 +1364,7 @@
                    z20 {y} zy with SUP.x<sup sp1 ?
                    ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p ))
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
-           z14 :  f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 ))
+           z14 :  f (& (SUP.sup (sp0 f mf as0 ? ))) ≡ & (SUP.sup (sp0 f mf as0 ? ))
            z14 = ? -- with ?
 --           ... | tri< a ¬b ¬c = ⊥-elim z16 where
 --               z16 : ⊥
@@ -1381,14 +1386,17 @@
      -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain
      --
      z04 :  (nmx : ¬ Maximal A ) → ⊥
-     z04 nmx = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as  sp1 ))))
-                                               (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) )
-           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) ))) -- x ≡ f x ̄
-           (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where          -- x < f x
-          sp1 : SUP A ?
-          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 
+     z04 nmx = ? where -- <-irr0  ? ? 
+           --(case1 ?)  -- x ≡ f x ̄
+           --  ? where          -- x < f x
+          sp1 : SUP A ? 
+          sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 ?
+          z041 : ?
+          z041 = cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) )
           c = & (SUP.sup sp1)
-
+          z042 : ?
+          z042 = is-cf nmx (SUP.as  ? )
+          z043 = proj1 (cf-is-<-monotonic nmx ? (SUP.as ? ))
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x  = zorn02 } where