# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1651261266 -32400
# Node ID 9ba98ecfbe626ceafed5dfe5ed07e79e1082fb4f
# Parent  fed1c67b9a656d9d2e12e76deddf3cdc092a9078
fcn-cmp done

diff -r fed1c67b9a65 -r 9ba98ecfbe62 src/zorn.agda
--- a/src/zorn.agda	Sat Apr 30 01:49:39 2022 +0900
+++ b/src/zorn.agda	Sat Apr 30 04:41:06 2022 +0900
@@ -107,20 +107,32 @@
 
 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-inject {A} s {x} {y} {f} mf cx cy eq = fc00 (fcn s mf cx) (fcn s mf cy) eq cx cy refl refl where
+     fc00 :  (i j : ℕ ) → i ≡ j  →  {x y : Ordinal } → (cx : FClosure A f s x ) (cy : FClosure A f s y ) → i ≡ fcn s mf cx  → j ≡ fcn s mf cy → * x ≡ * y
+     fc00 zero zero refl (init _) (init x₁) i=x i=y = refl
+     fc00 zero zero refl (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 zero refl (init sa) cy i=x i=y )
+     fc00 zero zero refl (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 zero refl cx (init sa) i=x i=y )
+     fc00 zero zero refl (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 zero refl cx cy  i=x i=y )
+     fc00 (suc i) (suc j) i=j {.(f x)} {.(f y)} (fsuc x cx) (fsuc y cy) i=x j=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) (suc j) i=j cx cy  i=x j=y )
+     ... | case1 x=fx | case2 y<fy = subst (λ k → k ≡ * (f y)) x=fx (fc02 x cx i=x) where
+          fc02 : (x1 : Ordinal) → (cx1 : FClosure A f s x1 ) →  suc i ≡ fcn s mf cx1 → * x1 ≡ * (f y)
+          fc02 .(f x1) (fsuc x1 cx1) i=x1 with proj1 (mf x1 (A∋fc s f mf cx1 ) )
+          ... | case1 eq = trans (sym eq) ( fc02  x1 cx1 i=x1 )  
+          ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc04) where
+               fc04 : * x1 ≡ * y
+               fc04 = fc00 i j (cong pred i=j) cx1 cy (cong pred i=x1) (cong pred j=y)
+     ... | case2 x<fx | case1 y=fy = subst (λ k → * (f x) ≡ k ) y=fy (fc03 y cy j=y) where
+          fc03 : (y1 : Ordinal) → (cy1 : FClosure A f s y1 ) →  suc j ≡ fcn s mf cy1 → * (f x)  ≡ * y1
+          fc03 .(f y1) (fsuc y1 cy1) j=y1 with proj1 (mf y1 (A∋fc s f mf cy1 ) )
+          ... | case1 eq = trans ( fc03  y1 cy1 j=y1 ) eq 
+          ... | case2 lt = subst₂ (λ j k → * (f j) ≡ * (f k )) &iso &iso ( cong (λ k → * ( f (& k ))) fc05) where
+               fc05 : * x ≡ * y1
+               fc05 = fc00 i j (cong pred i=j) cx cy1 (cong pred i=x) (cong pred j=y1)
+     ... | case2 x₁ | case2 x₂ = subst₂ (λ j k → * (f j) ≡ * (f k) ) &iso &iso (cong (λ k → * (f (& k))) (fc00 i j (cong pred i=j) cx cy (cong pred i=x) (cong pred j=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
@@ -137,31 +149,42 @@
           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 )
+fcn-cmp : {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 ) → Tri (* x < * y) (* x ≡ * y) (* y < * x )
-fcn-cmp {A} s {.s} {.s} f mf imm (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )
-fcn-cmp {A} s   f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) )
-... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy )
-... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where
-     lt : * s < * (f y)
-     lt with s≤fc  s f mf cy
-     ... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y
-     ... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y
-fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc  s f mf cx 
-... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt)
-... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt)  (λ eq → <-irr (case1 eq) s<x  ) s<x
-fcn-cmp {A} s   f mf imm (fsuc x cx) (fsuc y cy) 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 = {!!}
-... | case1 x=fx | case2 y<fy = {!!}
-... | 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 = {!!}
-     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 = {!!}
-     ... | tri≈ ¬a b ¬c = {!!}
-     ... | tri> ¬a ¬b c = {!!}
+fcn-cmp {A} s {x} {y} f mf cx cy with <-cmp ( fcn s mf cx ) (fcn s mf cy )
+... | tri< a ¬b ¬c = tri< fc11 (λ eq → <-irr (case1 (sym eq)) fc11) (λ lt → <-irr (case2 fc11) lt) where
+      fc11 : * x < * y
+      fc11 = fcn-< {A} s {x} {y} {f} mf cx cy a
+... | tri≈ ¬a b ¬c = tri≈ (λ lt → <-irr (case1 (sym fc10)) lt) fc10 (λ lt → <-irr (case1 fc10) lt) where
+      fc10 : * x ≡ * y
+      fc10 = fcn-inject {A} s {x} {y} {f} mf cx cy b
+... | tri> ¬a ¬b c = tri> (λ lt → <-irr (case2 fc12) lt) (λ eq → <-irr (case1 eq) fc12) fc12  where 
+      fc12 : * y < * x
+      fc12 = fcn-< {A} s {y} {x} {f} mf cy cx c
+
+-- fcn-cmp {A} s {.s} {.s} f mf (init x) (init x₁) = tri≈ (λ lt → <-irr (case1 refl) lt ) refl (λ lt → <-irr (case1 refl) lt )
+-- fcn-cmp {A} s   f mf imm (init x) (fsuc y cy) with proj1 (mf y (A∋fc s f mf cy ) )
+-- ... | case1 fy=y = subst (λ k → Tri (* s < * k) (* s ≡ * k) (* k < * s ) ) (*≡*→≡ fy=y) ( fcn-cmp {A} s f mf imm (init x) cy )
+-- ... | case2 fy>y = tri< lt (λ eq → <-irr (case1 (sym eq)) lt ) (λ lt1 → <-irr (case2 lt1) lt ) where
+--      lt : * s < * (f y)
+--      lt with s≤fc  s f mf cy
+--      ... | case1 s=y = subst (λ k → * k < * (f y) ) (sym (*≡*→≡ s=y)) fy>y
+--      ... | case2 s<y = IsStrictPartialOrder.trans PO s<y fy>y
+-- fcn-cmp {A} s {x} f mf imm cx (init x₁) with s≤fc  s f mf cx 
+-- ... | case1 eq = tri≈ (λ lt → <-irr (case1 eq) lt) (sym eq) (λ lt → <-irr (case1 (sym eq)) lt)
+-- ... | case2 s<x = tri> (λ lt → <-irr (case2 s<x) lt)  (λ eq → <-irr (case1 eq) s<x  ) s<x
+-- fcn-cmp {A} s   f mf imm (fsuc x cx) (fsuc y cy) 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 = {!!}
+-- ... | case1 x=fx | case2 y<fy = {!!}
+-- ... | 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 = {!!}
+--      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 = {!!}
+--      ... | tri≈ ¬a b ¬c = {!!}
+--      ... | tri> ¬a ¬b c = {!!}
 
 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
    field