# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651215131 -32400
# Node ID 726b6dac5eaafa6143244902978d65204648e227
# Parent  0687736285ce9c0953eaf97fce3e49850e180ad8
...

diff -r 0687736285ce -r 726b6dac5eaa src/zorn.agda
--- a/src/zorn.agda	Fri Apr 29 14:49:25 2022 +0900
+++ b/src/zorn.agda	Fri Apr 29 15:52:11 2022 +0900
@@ -15,6 +15,10 @@
 open import Data.Empty 
 import BAlgbra 
 
+open import Data.Nat hiding ( _<_ ; _≤_ )
+open import Data.Nat.Properties 
+open import nat 
+
 
 open inOrdinal O
 open OD O
@@ -74,39 +78,54 @@
 
 data FClosure (A : HOD) (f : Ordinal → Ordinal ) (s : Ordinal) : Ordinal → Set n where
    init : odef A s → FClosure A f s s
-   fsuc : {x : Ordinal} ( p :  FClosure A f s x ) → FClosure A f s (f x)
-
-open import Data.Nat hiding ( _<_ ; _≤_ )
-open import Data.Nat.Properties 
-open import nat 
-
-fcn : {A : HOD} {s x : Ordinal} {f : Ordinal → Ordinal} → FClosure A f s x → ℕ
-fcn (init as) = zero
-fcn (fsuc p) = suc ( fcn p )
-
-fcn-inject : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn fcx ≡ fcn fcy → x ≡ y
-fcn-inject f (init x) (init x₁) refl = refl
-fcn-inject f (fsuc fcx) (fsuc fcy) eq = cong f ( fcn-inject f fcx fcy ( cong pred eq ))
+   fsuc : (x : Ordinal) ( p :  FClosure A f s x ) → FClosure A f s (f x)
 
 A∋fc : {A : HOD} {s y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y
 A∋fc {A} {s} {.s} f mf (init as) = as
-A∋fc {A} {s}  f mf (fsuc {y} fcy) = proj2 (mf y ( A∋fc {A} {s}  f mf fcy ) )
+A∋fc {A} {s}  f mf (fsuc y fcy) = proj2 (mf y ( A∋fc {A} {s}  f mf fcy ) )
+
+fcn : {A : HOD} {s x : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → FClosure A f s x → ℕ
+fcn mf (init as) = zero
+fcn {A} {s} {x} {f} mf (fsuc y p) with mf y (A∋fc f mf p)
+... | ⟪ case1 eq , _ ⟫ = fcn mf p
+... | ⟪ case2 y<fy , _ ⟫ = suc (fcn mf p )
+
+ncf : {A : HOD} {s : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → ℕ → Ordinal
+ncf {A} {s} mf zero = s
+ncf {A} {s} {f} mf (suc x) = f (ncf {A} {s} mf x )
+
+FC→ : {A : HOD} {s : Ordinal} {f : Ordinal → Ordinal} → (mf : ≤-monotonic-f A f) → (x : ℕ ) → (fc :  FClosure A f s (ncf {A} {s} mf x) ) → fcn mf fc ≡ x
+FC→ {A} {s} {f} mf zero (init x) = refl
+FC→ {A} {.(f x)} {f} mf zero (fsuc x fc) = {!!}
+FC→ {A} {s} {f} mf (suc x) fc = {!!}
+
+fcn-inject : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) → (mf : ≤-monotonic-f A f)
+   → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn mf fcx ≡ fcn mf fcy → x ≡ y
+fcn-inject f mf (init x) (init x₁) refl = refl
+fcn-inject {A} {s} f mf (init sa) (fsuc y fcy) eq with proj1 (mf y (A∋fc f mf fcy ))
+... | case1 y=fy = subst (λ k → s ≡ k ) (subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) y=fy )) (fcn-inject f mf (init sa) fcy (trans eq fcn0 )) where
+    fcn0 : fcn mf ( fsuc y fcy ) ≡ fcn mf fcy
+    fcn0 with mf y (A∋fc f mf fcy )
+    ... | ⟪ case1 x , proj4 ⟫ = refl
+... | case2 y<fy = {!!}
+fcn-inject f mf (fsuc x fcx) (init sa) eq = {!!} -- cong f ( fcn-inject f mf fcx fcy ( cong pred eq ))
+fcn-inject f mf (fsuc x fcx) (fsuc y fcy) eq = {!!} -- cong f ( fcn-inject f mf fcx fcy ( cong pred eq ))
 
 fcn-cmp : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f)
     → (cx : FClosure A f s x) → (cy : FClosure A f s y ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
-fcn-cmp {A} {s} {x} {y} f mf cx cy with <-cmp (fcn cx) (fcn cy)
+fcn-cmp {A} {s} {x} {y} f mf cx cy with <-cmp (fcn mf cx) (fcn mf cy)
 ... | t = {!!}
 
 fcn-mono : {A : HOD} {s x y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f)
    → (imm : { x y : Ordinal } → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) )
-   → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn fcx Data.Nat.≤ fcn fcy → * x ≤ * y
+   → (fcx : FClosure A f s x) → (fcy : FClosure A f s y ) → fcn mf fcx Data.Nat.≤ fcn mf fcy → * x ≤ * y
 fcn-mono f mf imm (init _) (init _) z≤n = case1 refl
-fcn-mono {A} {s} {x} f mf imm (init sa) (fsuc {y} fcy) z≤n with proj1 (mf y (A∋fc f mf fcy ) ) 
+fcn-mono {A} {s} {x} f mf imm (init sa) (fsuc y fcy) z≤n with proj1 (mf y (A∋fc f mf fcy ) ) 
 ... | case1 eq = subst (λ k → * s ≤ k ) eq ( fcn-mono f mf imm (init sa) fcy z≤n )
 ... | case2 lt = ≤-ftrans (fcn-mono f mf imm (init sa) fcy z≤n) (case2 lt) 
-fcn-mono f mf imm (fsuc fcx) (fsuc fcy) (s≤s lt) with fcn-mono f mf imm fcx fcy lt
+fcn-mono f mf imm (fsuc x fcx) (fsuc y fcy) lt with fcn-mono f mf imm fcx fcy {!!}
 ... | case1 x=y = case1 (subst₂ (λ j k → * (f j) ≡ * (f k)) &iso &iso ( cong (λ k → * (f (& k ))) x=y )  )
-... | case2 x<y with <-cmp (fcn fcx) (fcn fcy)
+... | case2 x<y with <-cmp (fcn mf fcx) (fcn mf fcy)
 ... | tri< a ¬b ¬c = {!!}
 ... | tri≈ ¬a b ¬c = {!!}
 ... | tri> ¬a ¬b c = {!!}