# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649978081 -32400
# Node ID 99b8ea24e6cd9bd29608ffe1577bb4461ec08fc5
# Parent  dfcb98151273d917d2eaeacfaf81e4fe19fef859
...

diff -r dfcb98151273 -r 99b8ea24e6cd src/zorn.agda
--- a/src/zorn.agda	Wed Apr 13 09:54:01 2022 +0900
+++ b/src/zorn.agda	Fri Apr 15 08:14:41 2022 +0900
@@ -148,6 +148,24 @@
 IChainSet {A} ax = record { od = record { def = λ y → odef A y ∧ IChained A (& (elm ax)) y }
     ; odmax = & A ; <odmax = λ {y} lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 lt))) } 
 
+IC-is-total : {A : HOD} → (ax : Element A ) → IsPartialOrderSet A → IsTotalOrderSet (IChainSet {A} ax)
+IC-is-total {A} ax PO = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO
+   ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
+    IPO : IsPartialOrderSet (IChainSet {A} ax)
+    IPO = ⊆-IsPartialOrderSet record { incl = λ {x} lt → proj1 lt } PO
+    cmp : Trichotomous _ _ 
+    cmp x y with IChained.iy (proj2 (is-elm x)) | IChained.iy (proj2 (is-elm y))
+    ... | ifirst x₁ | ifirst x₂ = tri≈ {!!} {!!} {!!} 
+    ... | ifirst x₁ | inext x₂ x₃ s = {!!}
+    ... | inext x₁ x₂ t | ifirst x₃ = {!!}
+    ... | inext x₁ x₂ t | inext x₃ x₄ s with cmp (me ⟪ subst (λ k → odef A k) (sym &iso) (ic→odef t) ,
+      record { iy = subst (λ k → IChain A k) (sym &iso) t ; ic = ic1 } ⟫) (me ⟪ subst (λ k → odef A k) (sym &iso) (ic→odef s) ,
+      record { iy = subst (λ k → IChain A k) (sym &iso) s ; ic = ic2 } ⟫) where 
+        ic1 :  ic-connect (& (elm ax)) (subst (λ k → IChain A k) (sym &iso) t)
+        ic1 = {!!}
+        ic2 :  ic-connect (& (elm ax)) (subst (λ k → IChain A k) (sym &iso) s)
+        ic2 = {!!}
+    ... | t = {!!}
 -- there is a y, & y > & x
 
 record OSup> (A : HOD) {x : Ordinal} (ax : A ∋ * x) : Set n where
@@ -184,9 +202,9 @@
 --
 -- possible three cases in a limit ordinal step
 -- 
--- case 1) < goes > x
+-- case 1) < goes > x                       (will contradic in the transfinite induction )
 -- case 2) no > x in some chain ( maximal )
--- case 3) countably infinite chain below x
+-- case 3) countably infinite chain below x (will be prohibited by sup condtion )
 --
 Zorn-lemma-3case : { A : HOD } 
     → o∅ o< & A 
@@ -225,7 +243,7 @@
                 (subst (λ k → ic-connect (& k) (IChained.iy (proj2 zc5)) ) (me-elm-refl A x) (IChained.ic (proj2 zc5)) )  )
             zc6 : elm x < z
             zc6 = IsStrictPartialOrder.trans PO {x} {me (proj1 zc3)} {me az} zc7 y<z
-    ... | yes  nohg = case2 (case2 {!!} )
+    ... | yes inifite = case2 (case2 record {  chain<x = {!!} ;  c-infinite = {!!}  } )
 
 
 record SUP ( A B : HOD )  : Set (suc n) where
@@ -239,68 +257,23 @@
     → IsPartialOrderSet A 
     → ( ( B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → SUP A B   ) -- SUP condition
     → Maximal A 
-Zorn-lemma {A}  0<A PO supP = zorn00 where
-     someA : HOD
-     someA = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
-     isSomeA : A ∋ someA
-     isSomeA =  ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) 
-     HasMaximal : HOD
-     HasMaximal = record { od = record { def = λ y → odef A y ∧ ((m : Ordinal) →  odef A m → ¬ (* y < * m))} ; odmax = & A ; <odmax = z08 } where
-         z08 : {y : Ordinal} → (odef A y ∧ ((m : Ordinal) →  odef A m → ¬ (* y < * m)))  → y o< & A
-         z08 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P)))
-     no-maximal : HasMaximal =h= od∅ → (y : Ordinal) →  (odef A y ∧ ((m : Ordinal) →  odef A m → ¬ (* y < * m))) →  ⊥
-     no-maximal nomx y P = ¬x<0 (eq→ nomx {y} ⟪ proj1 P , (λ m am → (proj2 P) m am ) ⟫ ) 
-     Gtx : { x : HOD} → A ∋ x → HOD
-     Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z09 }  where
-         z09 : {y : Ordinal} → (odef A y ∧ (x < (* y)))  → y o< & A
-         z09 {y} P = subst (λ k → k o< & A) &iso (c<→o< {* y} (subst (λ k → odef A k) (sym &iso) (proj1 P)))
+Zorn-lemma {A}  0<A PO supP = zorn04 where
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
      z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋a} (sym a=b) b<a
      z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO {me A∋b} {me A∋b} refl (IsStrictPartialOrder.trans PO {me A∋b} {me A∋a} {me A∋b}  b<a a<b)
+     z02 : {x : Ordinal } → (ax : A ∋ * x ) → InFiniteIChain A  ax  → ⊥
+     z02 {x} ax ic = zc5 ic where
+              FC : HOD
+              FC = IChainSet {A} (me ax)
+              zc6 :  InFiniteIChain A ax  → ¬ SUP A FC 
+              zc6 inf = {!!}
+              FC-is-total : IsTotalOrderSet FC
+              FC-is-total = {!!}
+              FC⊆A :  FC ⊆ A
+              FC⊆A = record { incl = λ {x} lt → proj1 lt }
+              zc5 : InFiniteIChain A ax → ⊥
+              zc5 x = zc6 x ( supP FC FC⊆A FC-is-total )
      -- ZChain is not compatible with the SUP condition
-     record BX (x y : Ordinal) (fb : ( x : Ordinal ) → HOD ) : Set n where
-        field
-            bx : Ordinal
-            bx<y : bx o< y
-            is-fb : x ≡ & (fb bx )
-     bx<A : (z : ZChain A (& A) ) → {x : Ordinal } → (bx : BX x (& A) {!!})  → BX.bx bx o< & A
-     bx<A z {x} bx = BX.bx<y bx
-     z12 : (z : ZChain A (& A) ) →  {y : Ordinal} → BX y (& A) {!!} → y o< & A
-     z12 z {y} bx = subst (λ k → k o< & A) (sym (BX.is-fb bx)) (c<→o< {!!})  
-     B :  (z : ZChain A (& A) ) → HOD
-     B z = {!!}
-     z11 :  (z : ZChain A (& A) ) → (x : Element (B z)) → elm x ≡  {!!} 
-     z11 z x = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) (BX.is-fb (is-elm x)) )
-     obx : (z : ZChain A (& A) ) → {x : HOD} → B z ∋ x → Ordinal
-     obx z {x} bx = BX.bx bx
-     obx=fb : (z : ZChain A (& A) ) → {x : HOD} → (bx : B z ∋ x ) → x ≡ {!!}
-     obx=fb z {x} bx = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (BX.is-fb bx)) 
-     B⊆A : (z : ZChain A (& A) ) → B z ⊆ A
-     B⊆A z = record { incl = λ {x} bx → subst (λ k → odef A k ) (sym (BX.is-fb bx)) {!!}  }
-     -- PO-B : (z : ZChain A (& A) ) → IsPartialOrderSet (B z) _<_
-     -- PO-B z = ⊆-IsPartialOrderSet (B⊆A z) PO
-     bx-monotonic : (z : ZChain A (& A) ) → {x y : Element (B z)} → obx z (is-elm x) o< obx z (is-elm y) → elm x < elm y 
-     bx-monotonic z {x} {y} a = subst₂ (λ j k → j < k ) (sym (z11 z x)) (sym (z11 z y)) {!!}  
-     bcmp : (z : ZChain A (& A) ) → Trichotomous (λ (x : Element (B z)) y → elm x ≡ elm y ) (λ x y → elm x < elm y )
-     bcmp z x y with trio< (obx z (is-elm x)) (obx z (is-elm y))
-     ... | tri< a ¬b ¬c = tri< z15 (λ eq → z01 (incl (B⊆A z) (is-elm y)) (incl (B⊆A z) (is-elm x))(case1 (sym eq)) z15 ) z17 where
-          z15 :  elm x < elm y
-          z15 =  bx-monotonic z {x} {y} a
-          z17 : elm y < elm x → ⊥
-          z17 lt =  z01 (incl (B⊆A z) (is-elm y)) (incl (B⊆A z) (is-elm x))(case2 lt) z15 
-     ... | tri≈ ¬a b ¬c = tri≈ (IsStrictPartialOrder.irrefl PO {isA (B⊆A z) x} {isA (B⊆A z) y} z14) z14 z16 where
-          z14 :  elm x ≡ elm y
-          z14 = {!!}
-          z16 = IsStrictPartialOrder.irrefl PO {isA (B⊆A z) y} {isA (B⊆A z) x} (sym z14)
-     ... | tri> ¬a ¬b c = tri> z17 (λ eq → z01 (incl (B⊆A z) (is-elm x)) (incl (B⊆A z) (is-elm y))(case1 eq) z15 ) z15 where
-          z15 :  elm y < elm x
-          z15 =  bx-monotonic z {y} {x} c
-          z17 : elm x < elm y → ⊥
-          z17 lt =  z01 (incl (B⊆A z) (is-elm x)) (incl (B⊆A z) (is-elm y))(case2 lt) z15 
-     B-is-total :  (z : ZChain A (& A) ) → IsTotalOrderSet (B z) 
-     B-is-total zc = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
-         ; trans = λ {x} {y} {z} x<y y<z → IsStrictPartialOrder.trans PO {isA (B⊆A zc) x} {isA (B⊆A zc) y} {isA (B⊆A zc) z} x<y y<z
-         ; compare = bcmp zc }
      ind : (x : Ordinal) → ((y : Ordinal) → y o< x →  ZChain A y ∨ Maximal A )
          →  ZChain A x ∨ Maximal A 
      --     has previous ordinal
@@ -338,9 +311,7 @@
           zc1 : OSup> A (subst (OD.def (od A)) (sym &iso) ax) → ZChain A x ∨ Maximal A
           zc1 os with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
           ... | case2 x = case2 x
-          ... | case1 x with is-o∅ ( & (Gtx ax ))
-          ... | yes no-sup = case2 {!!}
-          ... | no sup = case1 {!!}
+          ... | case1 x = {!!}
           zc4 : ZChain A x ∨ Maximal A
           zc4 with Zorn-lemma-3case 0<A PO (me ax)
           ... | case1 y>x = zc1 y>x
@@ -364,35 +335,14 @@
      ... | tri≈ ¬a b ¬c = {!!} where
      ... | tri> ¬a ¬b c with ODC.∋-p O A (* x)
      ... | no ¬Ax = {!!} where
-     ... | yes ax with is-o∅ (& (Gtx ax))
-     ... | yes nogt = ⊥-elim {!!} where -- no larger element, so it is maximal
-              x-is-maximal :  (m : Ordinal) → odef A m → ¬ (* x < * m)
-              x-is-maximal m am  =  ¬x<m   where
-                 ¬x<m :  ¬ (* x < * m)
-                 ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫  (≡o∅→=od∅ nogt) 
+     ... | yes ax = {!!}
      ... | no not = {!!} where
      zorn03 : (x : Ordinal) → ZChain A x  ∨ Maximal A 
-     zorn03 x with TransFinite ind  x
-     ... | t = {!!}
+     zorn03 x = TransFinite ind  x
      zorn04 : Maximal A 
      zorn04 with zorn03 (& A)
-     ... | case1 chain = {!!}
+     ... | case1 chain = ⊥-elim ( o<> (c<→o< {ZChain.max chain} {A} (ZChain.A∋max chain))  (ZChain.y<max chain) )
      ... | case2 m = m
-     zorn00 : Maximal A 
-     zorn00 with is-o∅ ( & HasMaximal )
-     ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where
-         -- yes we have the maximal
-         hasm :  odef HasMaximal ( & ( ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ) )
-         hasm =  ODC.x∋minimal  O HasMaximal  (λ eq → not (=od∅→≡o∅ eq))
-         zorn01 :  A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq))
-         zorn01 =  proj1 hasm
-         zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x)
-         zorn02 {x} ax m<x = ((proj2 hasm) (& x) ax) (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x )
-     ... | yes ¬Maximal = {!!} where
-         -- if we have no maximal, make ZChain, which contradict SUP condition
-         z : (x : Ordinal) → HasMaximal =h= od∅  → ZChain A x  ∨ Maximal A 
-         z x nomx with TransFinite {!!} x
-         ... | t = {!!}
 
 -- _⊆'_ : ( A B : HOD ) → Set n
 -- _⊆'_ A B = (x : Ordinal ) → odef A x → odef B x