# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1650077503 -32400
# Node ID 97c8abf287062d6423175d97b1e32b9a3228705a
# Parent  5077d708f32f03d2b2dafdf192bf4dfe212c2f5c
...

diff -r 5077d708f32f -r 97c8abf28706 src/zorn.agda
--- a/src/zorn.agda	Sat Apr 16 01:12:50 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 11:51:43 2022 +0900
@@ -177,32 +177,38 @@
 import Data.Nat.Properties as NP
 open import nat
 
-data Chain (A : HOD) (s : Ordinal) (next : (x : Ordinal ) → odef A x → Ordinal ) : ( x : Ordinal  ) → Set n where
+data Chain (A : HOD) (s : Ordinal) (next : Ordinal  → Ordinal ) : ( x : Ordinal  ) → Set n where
      cfirst : odef A s → Chain A s next s
-     csuc : (x : Ordinal ) → (ax : odef A x ) → Chain A s next x → odef A (next x ax) → Chain A s next (next x ax )
+     csuc : (x : Ordinal ) → (ax : odef A x ) → Chain A s next x → odef A (next x) → Chain A s next (next x )
 
-ct∈A : (A : HOD ) (s : Ordinal)  → (next : (x : Ordinal ) → odef A x → Ordinal ) → {x : Ordinal} → Chain A s next x → odef A x
+ct∈A : (A : HOD ) (s : Ordinal)  → (next : Ordinal  → Ordinal ) → {x : Ordinal} → Chain A s next x → odef A x
 ct∈A A s next {x} (cfirst x₁) = x₁ 
-ct∈A A s next {.(next x ax)} (csuc x ax t anx) = anx
+ct∈A A s next {.(next x )} (csuc x ax t anx) = anx
 
-ChainClosure : (A : HOD) (s : Ordinal) →  (next : (x : Ordinal ) → odef A x → Ordinal ) → HOD
+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
     cc01 {y} cy = subst (λ k → k o< & A ) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) ( ct∈A A s next cy ) ) )
 
-cton0 : (A : HOD ) (s : Ordinal) → (next : (x : Ordinal ) → odef A x → Ordinal )  {y : Ordinal } → Chain A s next y → ℕ
+cton0 : (A : HOD ) (s : Ordinal) → (next : Ordinal  → Ordinal )  {y : Ordinal } → Chain A s next y → ℕ
 cton0 A s next (cfirst _)  = zero
 cton0 A s next (csuc x ax z _) = suc (cton0 A s next z) 
-cton : (A : HOD ) (s : Ordinal)   → (next : (x : Ordinal ) → odef A x → Ordinal ) → Element (ChainClosure A s next) → ℕ
+cton : (A : HOD ) (s : Ordinal)   → (next : Ordinal → Ordinal ) → Element (ChainClosure A s next) → ℕ
 cton A s next y = cton0 A s next (is-elm y)
 
+cinext :  (A : HOD) {x : Ordinal } → (ax : A ∋ * x ) → (ifc : InFiniteIChain A ax ) → Ordinal  →  Ordinal
+cinext A ax ifc y with ODC.∋-p O (IChainSet (me ax)) (* y)
+... | yes ics-y = IChainSup>.y ( InFiniteIChain.c-infinite ifc y (subst (λ k → odef (IChainSet (me ax)) k) &iso ics-y ))
+... | no _ = o∅
+
 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 ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) 
+InFCSet A {x} ax ifc =  ChainClosure (IChainSet {A} (me ax)) x {!!} -- (λ y → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) 
 
 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 (λ y ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) lt ) }
+     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 ) }
 
 ChainClosure-is-total : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → IsPartialOrderSet A 
@@ -213,14 +219,13 @@
     IPO : IsPartialOrderSet (InFCSet A ax ifc )
     IPO = ⊆-IsPartialOrderSet record { incl = λ {y} lt → incl (InFCSet⊆A A {x} ax ifc) lt} PO
     B = IChainSet {A} (me ax)
-    cnext :  (y : Ordinal ) → odef B y → Ordinal
-    cnext y ay = IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay  )
+    cnext = cinext A ax ifc
     ct02 : {oy : Ordinal} → (y : Chain B x cnext oy ) → A ∋ * oy 
     ct02 y = incl (IChainSet⊆A {A} (me ax)) (subst (λ k → odef (IChainSet (me ax)) k) (sym &iso) (ct∈A B x cnext y) ) 
     ct-inject : {ox oy : Ordinal} → (x1 : Chain B x cnext ox ) → (y : Chain B x cnext oy )
        → (cton0 B x cnext x1) ≡ (cton0 B x cnext y) → ox ≡ oy
     ct-inject {ox} {ox} (cfirst x) (cfirst x₁) refl = refl
-    ct-inject {.(cnext x₀ ax)} {.(cnext x₃ ax₁)} (csuc x₀ ax x₁ x₂) (csuc x₃ ax₁ y x₄) eq = {!!} where
+    ct-inject {.(cnext x₀ )} {.(cnext x₃ )} (csuc x₀ ax x₁ x₂) (csuc x₃ ax₁ y x₄) eq = cong cnext ct05 where
         ct06 : {x y : ℕ} → suc x ≡ suc y → x ≡ y
         ct06 refl = refl 
         ct05 : x₀ ≡ x₃
@@ -228,11 +233,16 @@
     ct-monotonic : {ox oy : Ordinal} → (x1 : Chain B x cnext ox ) → (y : Chain B x cnext oy )
        → (cton0 B x cnext x1) Data.Nat.< (cton0 B x cnext y) → * ox < * oy
     ct-monotonic {ox} {oy} x1 (csuc oy1 ay y _) (s≤s lt) with NP.<-cmp ( cton0 B x cnext x1 ) ( cton0 B x cnext y )
-    ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct03} (ct-monotonic x1 y a ) ct01  where
-        ct03 : A ∋ * (IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 ay))
-        ct03 = subst (λ k → odef A k ) (sym &iso) (IChainSup>.A∋y (InFiniteIChain.c-infinite ifc oy1 ay))
-        ct01 : * oy1 < * ( IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 ay) )
-        ct01 = (IChainSup>.y>x (InFiniteIChain.c-infinite ifc oy1 ay))
+    ... | tri< a ¬b ¬c = ct07 where
+        ct07 :  * ox < * (cnext oy1)
+        ct07 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 = IsStrictPartialOrder.trans PO {me (ct02 x1) } {me (ct02 y)} {me ct031 } (ct-monotonic x1 y a ) ct011 where
+           ct031 :  A ∋ * (IChainSup>.y (InFiniteIChain.c-infinite ifc oy1 (subst (λ k → odef (IChainSet {A} (me ax)) k) &iso ay1 ) )) 
+           ct031 = subst (λ k → odef A k ) (sym &iso) (
+              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 = {!!}
     cmp : Trichotomous _ _