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

diff -r 726b6dac5eaa -r ba889c711524 src/OD.agda
--- a/src/OD.agda	Fri Apr 29 15:52:11 2022 +0900
+++ b/src/OD.agda	Fri Apr 29 17:53:31 2022 +0900
@@ -186,6 +186,12 @@
 o≡→== : { x y : Ordinal  } → x ≡  y →  od (* x) == od (* y)
 o≡→==  {x} {.x} refl = ==-refl
 
+*≡*→≡ : { x y : Ordinal  } → * x ≡ * y →  x ≡ y
+*≡*→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) eq )
+
+&≡&→≡ : { x y : HOD  } → & x ≡  & y →  x ≡ y
+&≡&→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) eq )
+
 o∅≡od∅ : * (o∅ ) ≡ od∅ 
 o∅≡od∅  = ==→o≡ lemma where
      lemma0 :  {x : Ordinal} → odef (* o∅) x → odef od∅ x
diff -r 726b6dac5eaa -r ba889c711524 src/zorn.agda
--- a/src/zorn.agda	Fri Apr 29 15:52:11 2022 +0900
+++ b/src/zorn.agda	Fri Apr 29 17:53:31 2022 +0900
@@ -52,6 +52,10 @@
 ≤-ftrans {x} {_} {z} (case2 x<y ) (case1 refl ) = case2 x<y
 ≤-ftrans {x} {y} {z} (case2 x<y) (case2 y<z) = case2 ( IsStrictPartialOrder.trans PO x<y y<z )
 
+<-irr : {a b : HOD} → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
+<-irr {a} {b} (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
+<-irr {a} {b} (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
+          (IsStrictPartialOrder.trans PO     b<a a<b)
 
 open _==_
 open _⊆_
@@ -76,60 +80,50 @@
 ≤-monotonic-f : (A : HOD) → ( Ordinal → Ordinal ) → Set (Level.suc n)
 ≤-monotonic-f A f = (x : Ordinal ) → odef A x → ( * x ≤ * (f x) ) ∧  odef A (f x )
 
+immieate-f : (A : HOD) → ( f : Ordinal → Ordinal )  → Set n
+immieate-f A f = { x y : Ordinal } → odef A x → odef A y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) )
+
 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)
 
-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 : HOD} (s : Ordinal) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → odef A y
+A∋fc {A} 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 ) )
 
-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 = {!!}
+s≤fc : {A : HOD} (s : Ordinal ) {y : Ordinal } (f : Ordinal → Ordinal) (mf : ≤-monotonic-f A f) → (fcy : FClosure A f s y ) → * s ≤ * y
+s≤fc {A} s {.s} f mf (init x) = case1 refl
+s≤fc {A} s {.(f x)} f mf (fsuc x fcy) with proj1 (mf x (A∋fc s f mf fcy ) )
+... | case1 x=fx = subst (λ k → * s ≤ * k ) (*≡*→≡ x=fx) ( s≤fc {A} s f mf fcy )
+... | case2 x<fx with s≤fc {A} s f mf fcy 
+... | case1 s≡x = case2 ( subst₂ (λ j k → j < k ) (sym s≡x) refl x<fx )
+... | case2 s<x = case2 ( IsStrictPartialOrder.trans PO s<x x<fx )
 
-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)
+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 )
-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 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 ) ) 
-... | 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 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 mf fcx) (fcn mf fcy)
-... | tri< a ¬b ¬c = {!!}
-... | tri≈ ¬a b ¬c = {!!}
-... | tri> ¬a ¬b c = {!!}
--- = case2 {!!} -- * x < * y → * (f x) < * (f y)
+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 = {!!}
 
 record Prev< (A B : HOD) {x : Ordinal } (xa : odef A x)  ( f : Ordinal → Ordinal )  : Set n where
    field
@@ -169,9 +163,7 @@
      supO : (C : Ordinal ) → (* C) ⊆ A → IsTotalOrderSet (* C) → Ordinal
      supO C C⊆A TC = & ( SUP.sup ( supP (* C)  C⊆A TC ))
      z01 : {a b : HOD} → A ∋ a → A ∋ b  → (a ≡ b ) ∨ (a < b ) → b < a → ⊥
-     z01 {a} {b} A∋a A∋b (case1 a=b) b<a = IsStrictPartialOrder.irrefl PO   (sym a=b) b<a
-     z01 {a} {b} A∋a A∋b (case2 a<b) b<a = IsStrictPartialOrder.irrefl PO   refl
-          (IsStrictPartialOrder.trans PO     b<a a<b)
+     z01 {a} {b} A∋a A∋b = <-irr
      z07 :   {y : Ordinal} → {P : Set n} → odef A y ∧ P → y o< & A
      z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
      s : HOD