# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649726535 -32400
# Node ID 8ec0b88b022fd44e0bbe8207767158fe94d5a40e
# Parent  2a8629b5cff9053fda79fec98ef794d6ce2bb03b
zorn-case

diff -r 2a8629b5cff9 -r 8ec0b88b022f src/zorn.agda
--- a/src/zorn.agda	Mon Apr 11 15:14:53 2022 +0900
+++ b/src/zorn.agda	Tue Apr 12 10:22:15 2022 +0900
@@ -63,7 +63,7 @@
 ⊆-IsPartialOrderSet : { A B  : HOD } → B ⊆ A → IsPartialOrderSet A → IsPartialOrderSet B 
 ⊆-IsPartialOrderSet {A} {B} B⊆A  PA = record {
        isEquivalence = record { refl = refl ; sym = sym ; trans = trans } ;  trans = λ {x} {y} {z} → trans1 {x} {y} {z} 
-     ; irrefl = λ {x} {y} → irrefl1 {x} {y} ; trans = trans1 ; <-resp-≈ = resp0 
+     ; irrefl = λ {x} {y} → irrefl1 {x} {y} ; <-resp-≈ = resp0 
    } where
    _<B_ : (x y : Element B ) → Set n
    x <B y = elm x < elm y
@@ -100,7 +100,6 @@
       A∋maximal : A ∋ maximal
       ¬maximal<x : {x : HOD} → A ∋ x  → ¬ maximal < x       -- A is Partial, use negative
 
-
 record ZChain ( A : HOD ) (y : Ordinal)   : Set (suc n) where
    field
       max : HOD
@@ -110,7 +109,39 @@
       chain⊆A : chain ⊆ A  
       total : IsTotalOrderSet chain 
       chain-max : (x : HOD) → chain ∋ x → (x ≡ max ) ∨ ( x < max )
+
+data IChain  (A : HOD) : Ordinal → Set n where
+    ifirst : {ox : Ordinal} → odef A ox → IChain A ox
+    inext  : {ox oy : Ordinal} → odef A oy → * ox < * oy → IChain A ox → IChain A oy
+
+ic-connet :  {A : HOD} {x : Ordinal} → (x : IChain A x) → Ordinal →  Set n
+ic-connet {A} (ifirst {ox} ax) oy = ox ≡ oy
+ic-connet {A} (inext {ox} {oy} ay x<y iy) oz = (ox ≡ oz) ∨ ic-connet iy oz
+
+IChainSet : {A : HOD} → Element A → HOD
+IChainSet {A} ax = record { od = record { def = λ y → odef A y ∧ ( (iy : IChain A y ) → ic-connet iy (& (elm ax)))  }
+    ; odmax = & A ; <odmax = λ {y} lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 lt))) } 
+
+-- there is a y, & y > & x
+
+record Sup> {A : HOD} (x : Element A) : Set (suc n) where
+   field
+      y : Element A
+      y>x : IChainSet x ∋ elm y → & (elm x) o< & (elm y)
+
+-- finite IChain
+
+record InFiniteIChain {A : HOD} (x : Element A) : Set (suc n) where
+   field
+      y : Element A
+      y>x : IChainSet x ∋ elm y → elm x < elm y
       
+Zorn-lemma-case : { A : HOD } 
+    → o∅ o< & A 
+    → IsPartialOrderSet A 
+    → (x : Element A) → Sup> x ∨ Dec ( InFiniteIChain x )
+Zorn-lemma-case {A}  0<A PO x = {!!}
+
 Zorn-lemma : { A : HOD } 
     → o∅ o< & A 
     → IsPartialOrderSet A 
@@ -200,24 +231,24 @@
      --              else use the ordinaly smallest max as next chain
      ind x prev with Oprev-p x
      ... | yes op with ODC.∋-p O A (* x)
-     ... | no ¬Ax = {!!} where
+     ... | no ¬Ax = zc1 where
           -- we have previous ordinal and ¬ A ∋ x, use previous Zchain
           px = Oprev.oprev op
-          zc1 : ZChain A px 
+          zc1 : ZChain A x ∨ Maximal A
           zc1 with prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          ... | t = {!!}
-          z04 :  {!!} -- (sup : HOD) (as : A ∋ sup) → & sup o< osuc x → sup < ZChain.fb zc1 as
-          z04 sup as s<x with trio< (& sup) x
-          ... | tri≈ ¬a b ¬c = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans b (sym &iso)) as) )  
-          ... | tri< a ¬b ¬c  = {!!} -- ZChain.¬x<sup zc1 _ as ( subst (λ k → & sup o< k ) (sym (Oprev.oprev=x op)) a )
-          ... | tri> ¬a ¬b c with  osuc-≡< s<x
-          ... | case1 eq = ⊥-elim (¬Ax (subst (λ k → odef A k) (trans eq (sym &iso)) as) )  
-          ... | case2 lt = ⊥-elim (¬a lt )
-     ... | yes ax = {!!} where -- we have previous ordinal and A ∋ x
+          ... | case2 x = case2 x  -- we have the Maximal
+          ... | case1 z with trio< x (& (ZChain.max z))
+          ... | tri< a ¬b ¬c = case1 record { max = ZChain.max z ; y<max = a }
+          ... | tri≈ ¬a b ¬c = {!!} -- x = max so ¬ A ∋ max 
+          ... | tri> ¬a ¬b c = {!!} -- can't happen
+     ... | yes ax = zc1 where -- we have previous ordinal and A ∋ x
           px = Oprev.oprev op
-          zc1 : ZChain A px 
+          zc1 : ZChain A x ∨ Maximal A
           zc1 with  prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) 
-          ... | t = {!!}
+          ... | case2 x = case2 x
+          ... | case1 x with is-o∅ ( & (Gtx ax ))
+          ... | yes no-sup = case2 {!!}
+          ... | no sup = case1 {!!}
      ind x prev | no ¬ox with trio< (& A) x   --- limit ordinal case
      ... | tri< a ¬b ¬c = {!!} where
           zc1 : ZChain A (& A)