# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651250979 -32400
# Node ID fed1c67b9a656d9d2e12e76deddf3cdc092a9078
# Parent  f1e899cbe845fb6d62ba92d64e1db6cb8c9e4f79
...

diff -r f1e899cbe845 -r fed1c67b9a65 src/zorn.agda
--- a/src/zorn.agda	Fri Apr 29 18:23:49 2022 +0900
+++ b/src/zorn.agda	Sat Apr 30 01:49:39 2022 +0900
@@ -101,21 +101,41 @@
 
 fcn : {A : HOD} (s : Ordinal) { x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ
 fcn s mf (init as) = zero
-fcn {A} s {x} {f} mf (fsuc y p) with mf y (A∋fc f mf p)
-... | ⟪ case1 eq , _ ⟫ = fcn s mf p
-... | ⟪ case2 y<fy , _ ⟫ = suc (fcn s mf p )
+fcn {A} s {x} {f} mf (fsuc y p) with proj1 (mf y (A∋fc s f mf p))
+... | case1 eq = fcn s mf p
+... | case2 y<fy = suc (fcn s mf p )
 
-fcn-suc : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
-    → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → suc (fcn s mf cx ) ≡ fcn s mf cy  → * x < * y
-fcn-suc = ?
+fcn-inject : {A : HOD} (s : Ordinal) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) 
+     → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx  ≡ fcn s mf cy → * x ≡ * y
+fcn-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) cx cy refl eq where
+     fc00 :  (i : ℕ ) →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → i ≡ fcn s mf cy → * x ≡ * y
+     fc00 zero (init _) (init x₁) i=x i=y = refl
+     fc00 zero (init sa) (fsuc y cy) i=x i=y with proj1 (mf y (A∋fc s f mf cy ) )
+     ... | case1 y=fy = subst (λ k → * s ≡ k ) y=fy ( fc00 zero (init sa) cy i=x i=y )
+     fc00 zero (fsuc x cx) (init sa) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) )
+     ... | case1 x=fx = subst (λ k → k ≡ * s ) x=fx ( fc00 zero cx (init sa) i=x i=y )
+     fc00 zero (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
+     ... | case1 x=fx  | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 zero cx cy  i=x i=y )
+     fc00 (suc i) {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x i=y with proj1 (mf x (A∋fc s f mf cx ) ) | proj1 (mf y (A∋fc s f mf cy ) )
+     ... | case1 x=fx | case1 y=fy = subst₂ (λ j k → j ≡ k ) x=fx y=fy ( fc00 (suc i) cx cy  i=x i=y )
+     ... | case1 x=fx | case2 y<fy = {!!}
+     ... | case2 x<fx | case1 y=fy = {!!}
+     ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i cx cy (cong pred i=x) (cong pred i=y)))
 
 fcn-< : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
     → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → fcn s mf cx Data.Nat.< fcn s mf cy  → * x < * y
-fcn-< = ?
-
-fcn-fsuc : {A : HOD} (s : Ordinal ) { x y : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f)
-    → (cx : FClosure A f s x ) (cy : FClosure A f s (f x) ) → * x < * (f x)  → suc (fcn s mf cx ) ≡ fcn s mf cy  
-fcn-fsuc = ?
+fcn-< {A} s {x} {y} {f} mf cx cy x<y = fc01 (fcn s mf cy) cx cy refl x<y where
+     fc01 : (i : ℕ ) → {y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → (i ≡ fcn s mf cy ) → fcn s mf cx Data.Nat.< i → * x < * y
+     fc01 (suc i) {y} cx (fsuc y1 cy) i=y (s≤s x<i) with proj1 (mf y1 (A∋fc s f mf cy ) )
+     ... | case1 y=fy = subst (λ k → * x < k ) y=fy ( fc01 (suc i) {y1} cx cy i=y (s≤s x<i)  ) 
+     ... | case2 y<fy with <-cmp (fcn s mf cx ) i
+     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i c )
+     ... | tri≈ ¬a b ¬c = subst (λ k → k < * (f y1) ) (fcn-inject s mf cy cx (sym (trans b (cong pred i=y) ))) y<fy 
+     ... | tri< a ¬b ¬c = IsStrictPartialOrder.trans PO fc02 y<fy where
+          fc03 :  suc i ≡ suc (fcn s mf cy) → i ≡ fcn s mf cy
+          fc03 eq = cong pred eq 
+          fc02 :  * x < * y1 
+          fc02 =  fc01 i cx cy (fc03 i=y ) a
 
 fcn-cmp : {A : HOD} (s : Ordinal) { x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) (imm : immieate-f A f )
     → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
@@ -136,7 +156,7 @@
 ... | case2 x<fx | case1 y=fy = {!!}
 ... | case2 x<fx | case2 y<fy = {!!} where
      fc-mono : {x y : Ordinal } → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → FClosure A f x y ∨ FClosure A f y x
-     fc-mono = ?
+     fc-mono = {!!}
      fc1 :  Tri (* (f x) < * (f y)) (* (f x) ≡ * (f y)) (* (f y) < * (f x))
      fc1 with fcn-cmp s f mf imm cx cy
      ... | tri< a ¬b ¬c = {!!}