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

diff -r 7cf24b846920 -r 5077d708f32f src/zorn.agda
--- a/src/zorn.agda	Sat Apr 16 00:26:38 2022 +0900
+++ b/src/zorn.agda	Sat Apr 16 01:12:50 2022 +0900
@@ -177,30 +177,32 @@
 import Data.Nat.Properties as NP
 open import nat
 
-data Chain (A : HOD) (next : (x : Ordinal ) → odef A x → Ordinal ) : ( x : Ordinal  ) → Set n where
-     cfirst : (x : Ordinal ) → odef A x → Chain A next x
-     csuc : (x : Ordinal ) → (ax : odef A x ) → Chain A next x → odef A (next x ax) → Chain A next (next x ax )
+data Chain (A : HOD) (s : Ordinal) (next : (x : Ordinal ) → odef A x → 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 )
 
-ct∈A : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → {x : Ordinal} → Chain A next x → odef A x
-ct∈A A next {x} (cfirst .x x₁) = x₁ 
-ct∈A A next {.(next x ax)} (csuc x ax t anx) = anx
+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 s next {x} (cfirst x₁) = x₁ 
+ct∈A A s next {.(next x ax)} (csuc x ax t anx) = anx
 
-ChainClosure : (A : HOD) →  (next : (x : Ordinal ) → odef A x → Ordinal ) → HOD
-ChainClosure A  next = record { od = record { def = λ x → Chain A next x } ; odmax = & A ; <odmax = {!!} }
+ChainClosure : (A : HOD) (s : Ordinal) →  (next : (x : Ordinal ) → odef A x → 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 )  → (next : (x : Ordinal ) → odef A x → Ordinal )  {y : Ordinal } → Chain A next y → ℕ
-cton0 A next (cfirst _ x) = zero
-cton0 A next (csuc x ax z _) = suc (cton0 A next z) 
-cton : (A : HOD )  → (next : (x : Ordinal ) → odef A x → Ordinal ) → Element (ChainClosure A next) → ℕ
-cton A next y = cton0 A next (is-elm y)
+cton0 : (A : HOD ) (s : Ordinal) → (next : (x : Ordinal ) → odef A x → 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 s next y = cton0 A s next (is-elm y)
 
 InFCSet : (A : HOD) → {x : Ordinal}  (ax : A ∋ * x)
      → (ifc : InFiniteIChain A ax ) → HOD
-InFCSet A ax ifc =  ChainClosure (IChainSet {A} (me ax)) (λ y ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) 
+InFCSet A {x} ax ifc =  ChainClosure (IChainSet {A} (me ax)) x (λ y ay → 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)) (λ y ay → IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay ) ) 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,12 +215,20 @@
     B = IChainSet {A} (me ax)
     cnext :  (y : Ordinal ) → odef B y → Ordinal
     cnext y ay = IChainSup>.y ( InFiniteIChain.c-infinite ifc y ay  )
-    ct02 : {ox : Ordinal} → (x : Chain B cnext ox ) → A ∋ * ox 
-    ct02 x = incl (IChainSet⊆A {A} (me ax)) (subst (λ k → odef (IChainSet (me ax)) k) (sym &iso) (ct∈A B cnext x) ) 
-    ct-monotonic : {ox oy : Ordinal} → (x : Chain B cnext ox ) → (y : Chain B cnext oy )
-       → (cton0 B cnext x) Data.Nat.< (cton0 B cnext y) → * ox < * oy
-    ct-monotonic {ox} {oy} x (csuc oy1 ay y _) (s≤s lt) with NP.<-cmp ( cton0 B cnext x ) ( cton0 B cnext y )
-    ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO {me (ct02 x) } {me (ct02 y)} {me ct03} (ct-monotonic x y a ) ct01  where
+    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
+        ct06 : {x y : ℕ} → suc x ≡ suc y → x ≡ y
+        ct06 refl = refl 
+        ct05 : x₀ ≡ x₃
+        ct05 = ct-inject x₁ y (ct06 eq)
+    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) )
@@ -226,8 +236,10 @@
     ... | tri≈ ¬a b ¬c = {!!}
     ... | tri> ¬a ¬b c = {!!}
     cmp : Trichotomous _ _ 
-    cmp x y with NP.<-cmp (cton B cnext x) (cton B cnext y)
-    ... | tri< a ¬b ¬c = {!!}
+    cmp x1 y with NP.<-cmp (cton B x cnext x1) (cton B x cnext y)
+    ... | tri< a ¬b ¬c = tri< ct04 {!!} {!!} 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 = {!!}