--- a/src/zorn.agda	Sat Apr 16 12:20:08 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 16:09:14 2022 +0900
@@ -93,18 +93,18 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-postulate
-   ∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (ax : A ∋ x) (ay : A ∋ y ) → ax ≅ ay 
-   odef-irr : (A : OD) {x y : Ordinal} → x ≡ y → (ax : def A x) (ay : def A y ) → ax ≅ ay 
+-- postulate   -- may be proved by transfinite induction and functional extentionality
+--   ∋x-irr : (A : HOD) {x y : HOD} → x ≡ y → (ax : A ∋ x) (ay : A ∋ y ) → ax ≅ ay 
+--   odef-irr : (A : OD) {x y : Ordinal} → x ≡ y → (ax : def A x) (ay : def A y ) → ax ≅ ay 
 
-is-elm-irr : (A : HOD) → {x y : Element A } → elm x ≡ elm y → is-elm x ≅ is-elm y 
-is-elm-irr A {x} {y} eq = ∋x-irr A eq (is-elm x) (is-elm y )
+-- is-elm-irr : (A : HOD) → {x y : Element A } → elm x ≡ elm y → is-elm x ≅ is-elm y 
+-- is-elm-irr A {x} {y} eq = ∋x-irr A eq (is-elm x) (is-elm y )
 
 El-irr2 : (A : HOD) → {x y : Element A } → elm x ≡ elm y → is-elm x ≅ is-elm y → x ≡ y
 El-irr2  A {x} {y} refl HE.refl = refl
 
-El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y
-El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) 
+-- El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y
+-- El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) 
 
 record ZChain ( A : HOD ) (y : Ordinal)   : Set (Level.suc n) where
    field
@@ -169,7 +169,6 @@
 
 record InFiniteIChain (A : HOD) {x : Ordinal}  (ax : A ∋ * x) : Set n where
    field
-      chain<x : (y : Ordinal ) → odef (IChainSet {A} (me ax)) y →  y o< x
       c-infinite : (y : Ordinal ) → (cy : odef (IChainSet {A} (me ax)) y  )
           → IChainSup> A (ic→A∋y A ax cy)
 
@@ -185,6 +184,9 @@
 ct∈A A s next {x} (cfirst x₁) = x₁ 
 ct∈A A s next {.(next x )} (csuc x ax t anx) = anx
 
+--
+-- extract single chain from countable infinite chains
+--
 ChainClosure : (A : HOD) (s : Ordinal) →  (next : Ordinal → Ordinal ) → HOD
 ChainClosure A s next = record { od = record { def = λ x → Chain A s next x } ; odmax = & A ; <odmax = cc01 } where
     cc01 : {y : Ordinal} → Chain A s next y → y o< & A
@@ -203,12 +205,11 @@
 
 InFCSet : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → (ifc : InFiniteIChain A ax ) → HOD
-InFCSet A {x} ax ifc =  ChainClosure (IChainSet {A} (me ax)) x {!!} -- (λ y → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) 
+InFCSet A {x} ax ifc =  ChainClosure (IChainSet {A} (me ax)) x (cinext A ax ifc ) 
 
 InFCSet⊆A : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x) →  (ifc : InFiniteIChain A ax ) → InFCSet A ax ifc ⊆ A
 InFCSet⊆A A {x} ax ifc = record { incl = λ {y} lt → incl (IChainSet⊆A (me ax)) (
-     ct∈A (IChainSet {A} (me ax)) x {!!}  lt ) }
-     -- ct∈A (IChainSet {A} (me ax)) x (λ y ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) lt ) }
+     ct∈A (IChainSet {A} (me ax)) x (cinext A ax ifc) lt ) }
 
 ChainClosure-is-total : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → IsPartialOrderSet A 
@@ -243,15 +244,39 @@
               IChainSup>.A∋y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet {A} (me ax)) k) &iso ay1 )) )
            ct011 :  * oy1 < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet {A} (me ax)) k) &iso ay1 )) )
            ct011 = IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet {A} (me ax)) k) &iso ay1 )) 
-    ... | tri≈ ¬a b ¬c = {!!}
-    ... | tri> ¬a ¬b c = {!!}
+    ... | tri≈ ¬a b ¬c = ct11 where
+           ct11 : * ox < * (cnext oy1)
+           ct11 with ODC.∋-p O (IChainSet {A} (me ax)) (* oy1)
+           ... | no not  = ⊥-elim ( not (subst (λ k → odef (IChainSet {A} (me ax)) k ) (sym &iso) ay ) )
+           ... | yes ay1 = subst (λ k → * k < _) (sym (ct-inject _ _ b)) ct011  where
+              ct011 :  * oy1 < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet {A} (me ax)) k) &iso ay1 )) )
+              ct011 = IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet {A} (me ax)) k) &iso ay1 )) 
+    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c ) 
+    ct12 : {y z : Element (ChainClosure B x cnext) } → elm y ≡ elm z → elm y < elm z → ⊥ 
+    ct12 {y} {z} y=z y<z = IsStrictPartialOrder.irrefl IPO {y} {z} y=z y<z
+    ct13 : {y z : Element (ChainClosure B x cnext) } → elm y < elm z → elm z < elm y → ⊥ 
+    ct13 {y} {z} y<z y>z = IsStrictPartialOrder.irrefl IPO {y} {y} refl ( IsStrictPartialOrder.trans IPO {y} {z} {y} y<z y>z )
+    ct17 : (x1 : Element (ChainClosure B x cnext)) → Chain B x cnext (& (elm x1))
+    ct17 x1 = is-elm x1
     cmp : Trichotomous _ _ 
     cmp x1 y with NP.<-cmp (cton B x cnext x1) (cton B x cnext y)
-    ... | tri< a ¬b ¬c = tri< ct04 {!!} {!!} where
+    ... | tri< a ¬b ¬c = tri< ct04 ct14 ct15 where
         ct04 : elm x1 < elm y
         ct04 = subst₂ (λ j k → j < k  ) *iso *iso (ct-monotonic (is-elm x1) (is-elm y) a)
-    ... | tri≈ ¬a b ¬c = {!!}
-    ... | tri> ¬a ¬b c = {!!}
+        ct14 : ¬ elm x1 ≡  elm y
+        ct14 eq = ct12 {x1} {y} eq (subst₂ (λ j k → j < k ) *iso *iso (ct-monotonic (is-elm x1) (is-elm y) a )  )
+        ct15 : ¬ (elm y <  elm x1)
+        ct15 lt = ct13 {y} {x1} lt (subst₂ (λ j k → j < k ) *iso *iso (ct-monotonic (is-elm x1) (is-elm y) a )  )
+    ... | tri≈ ¬a b ¬c = tri≈ (ct12 {x1} {y} ct16)  ct16 (ct12 {y} {x1} (sym ct16)) where
+        ct16 :  elm x1 ≡ elm y
+        ct16 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (ct-inject {& (elm x1)} {& (elm y)} (is-elm x1) (is-elm y) b ))
+    ... | tri> ¬a ¬b c = tri> ct15 ct14 ct04 where
+        ct04 : elm y < elm x1
+        ct04 = subst₂ (λ j k → j < k  ) *iso *iso (ct-monotonic (is-elm y) (is-elm x1) c)
+        ct14 : ¬ elm x1 ≡  elm y
+        ct14 eq = ct12 {y} {x1} (sym eq) (subst₂ (λ j k → j < k ) *iso *iso (ct-monotonic (is-elm y) (is-elm x1) c )  )
+        ct15 : ¬ (elm x1 <  elm y)
+        ct15 lt = ct13 {x1} {y} lt (subst₂ (λ j k → j < k ) *iso *iso (ct-monotonic (is-elm y) (is-elm x1) c )  )
 
       
 record IsFC (A : HOD) {x : Ordinal}  (ax : A ∋ * x) (y : Ordinal) : Set n where
@@ -309,8 +334,12 @@
                 (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 inifite = case2 (case2 record {  chain<x = {!!} ;  c-infinite = {!!}  } )
+    ... | yes inifite = case2 (case2 record {    c-infinite = {!!}  } )
 
+all-climb-case : { A : HOD } → (0<A : o∅ o< & A) → IsPartialOrderSet A
+     → (( x : Element A) → OSup> A (d→∋ A (is-elm x) ))
+     → InFiniteIChain A (d→∋ A (ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ))
+all-climb-case {A} 0<A PO climb = record {    c-infinite = {!!}  } 
 
 record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
@@ -376,7 +405,7 @@
               B⊆A : (ifc : InFiniteIChain A ax)  →   B ifc ⊆ A
               B⊆A = {!!}
               ifc : InFiniteIChain A (subst (OD.def (od A)) (sym &iso) ax) → InFiniteIChain A ax
-              ifc record { chain<x = chain<x ; c-infinite = c-infinite } = record { chain<x = {!!} ; c-infinite = {!!} }  where
+              ifc record {  c-infinite = c-infinite } = record {  c-infinite = {!!} }  where
                   ifc01 : {!!} -- me (subst (OD.def (od A)) (sym &iso) ax)
                   ifc01 = {!!}
                -- (y : Ordinal) → odef (IChainSet (me (subst (OD.def (od A)) (sym &iso) ax))) y → y o< & (* x₁)