# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655718403 -32400
# Node ID 1150b006059bee88a0085739766000d1f93fb666
# Parent  d5cd551e0ed969271e2169294cc475e6f345e027
... give up

diff -r d5cd551e0ed9 -r 1150b006059b src/zorn.agda
--- a/src/zorn.agda	Mon Jun 20 17:39:28 2022 +0900
+++ b/src/zorn.agda	Mon Jun 20 18:46:43 2022 +0900
@@ -339,8 +339,9 @@
      --- the maximum chain  has fix point of any ≤-monotonic function
      ---
      fixpoint :  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f  (& A) )
+            → ( {x y : Ordinal} → x o≤ (& A) → IsTotalOrderSet (ZChain.chain zc) )
             → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc ))
-     fixpoint f mf zc = z14 where
+     fixpoint f mf zc total = z14 where
            chain = ZChain.chain zc
            sp1 = sp0 f mf zc
            z10 :  {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) 
@@ -366,31 +367,30 @@
                    ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p )
                    -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ?  (SUP.x<sup sp1 ? ) }
            z14 :  f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc))
-           z14 = {!!}
-           -- with ZChain.f-total zc {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
-           -- ... | tri< a ¬b ¬c = ⊥-elim z16 where
-           --     z16 : ⊥
-           --     z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
-           --     ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
-           --     ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
-           -- ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
-           -- ... | tri> ¬a ¬b c = ⊥-elim z17 where
-           --     z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
-           --     z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
-           --     z17 : ⊥
-           --     z17 with z15
-           --     ... | case1 eq = ¬b eq
-           --     ... | case2 lt = ¬a lt
+           z14 with total {& A} {& A} o≤-refl (subst (λ k → odef chain k) (sym &iso)  (ZChain.f-next zc z12 )) z12 
+           ... | tri< a ¬b ¬c = ⊥-elim z16 where
+               z16 : ⊥
+               z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 ))
+               ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) ))
+               ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt ))
+           ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b )
+           ... | tri> ¬a ¬b c = ⊥-elim z17 where
+               z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) <  SUP.sup sp1)
+               z15  = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 ))
+               z17 : ⊥
+               z17 with z15
+               ... | case1 eq = ¬b eq
+               ... | case2 lt = ¬a lt
 
      -- ZChain contradicts ¬ Maximal
      --
      -- 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) (& A)) → ⊥
-     z04 nmx zc = <-irr0  {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal  sp1))))
+     z04 :  (nmx : ¬ Maximal A ) → (zc : ZChain A (& s) (cf nmx) (& A)) → ({x y : Ordinal} → x o≤ & A → IsTotalOrderSet (ZChain.chain zc)) → ⊥
+     z04 nmx zc total = <-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 ̄
+           (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄
            (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where          -- x < f x
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc
           c = & (SUP.sup sp1)
@@ -538,6 +538,11 @@
                 sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) )
                 schain : HOD
                 schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy  }
+                supf0 : Ordinal → HOD
+                supf0 z with trio< z x
+                ... | tri< a ¬b ¬c = supf z
+                ... | tri≈ ¬a b ¬c = schain 
+                ... | tri> ¬a ¬b c = schain
                 A∋schain : {x : HOD } → schain ∋ x → A ∋ x
                 A∋schain (case1 zx ) = ZChain.chain⊆A zc zx 
                 A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx 
@@ -603,11 +608,6 @@
                      z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc )
                      ... | case1 y=b  = subst (λ k → odef chain0 k )  y=b ( ZChain.chain∋x zc )
                      ... | case2 y<b  = ZChain.is-max zc (ZChain.chain∋x zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b
-                supf0 : Ordinal → HOD
-                supf0 z with trio< z x
-                ... | tri< a ¬b ¬c = supf z
-                ... | tri≈ ¬a b ¬c = schain 
-                ... | tri> ¬a ¬b c = schain
                 seq : schain ≡ supf0 x 
                 seq with trio< x x
                 ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl )
@@ -722,7 +722,7 @@
          zorn01  = proj1  zorn03  
          zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
          zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
-     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04) where
+     ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04 {!!} ) where
          -- if we have no maximal, make ZChain, which contradict SUP condition
          nmx : ¬ Maximal A 
          nmx mx =  ∅< {HasMaximal} zc5 ( ≡o∅→=od∅  ¬Maximal ) where