# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1649993078 -32400
# Node ID d0ae1e3288f28bd713d19f1bded1891734eda931
# Parent  99b8ea24e6cd9bd29608ffe1577bb4461ec08fc5
...

diff -r 99b8ea24e6cd -r d0ae1e3288f2 src/zorn.agda
--- a/src/zorn.agda	Fri Apr 15 08:14:41 2022 +0900
+++ b/src/zorn.agda	Fri Apr 15 12:24:38 2022 +0900
@@ -1,5 +1,5 @@
 {-# OPTIONS --allow-unsolved-metas #-}
-open import Level
+open import Level hiding ( suc ; zero )
 open import Ordinals
 import OD 
 module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) where
@@ -40,18 +40,18 @@
 
 open HOD
 
-record Element (A : HOD) : Set (suc n) where
+record Element (A : HOD) : Set (Level.suc n) where
     field
        elm : HOD
        is-elm : A ∋ elm
 
 open Element
 
-IsPartialOrderSet : ( A : HOD ) → Set (suc n)
+IsPartialOrderSet : ( A : HOD ) → Set (Level.suc n)
 IsPartialOrderSet A = IsStrictPartialOrder _≡A_ _<A_  where
    _<A_ : (x y : Element A ) → Set n
    x <A y = elm x < elm y
-   _≡A_ : (x y : Element A ) → Set (suc n)
+   _≡A_ : (x y : Element A ) → Set (Level.suc n)
    x ≡A y = elm x ≡ elm y
 
 open _==_
@@ -78,11 +78,11 @@
 
 -- open import Relation.Binary.Properties.Poset as Poset
 
-IsTotalOrderSet : ( A : HOD ) →  Set (suc n)
+IsTotalOrderSet : ( A : HOD ) →  Set (Level.suc n)
 IsTotalOrderSet A = IsStrictTotalOrder  _≡A_ _<A_ where
    _<A_ : (x y : Element A ) → Set n
    x <A y = elm x < elm y
-   _≡A_ : (x y : Element A ) → Set (suc n)
+   _≡A_ : (x y : Element A ) → Set (Level.suc n)
    x ≡A y = elm x ≡ elm y
 
 me : { A a : HOD } → A ∋ a → Element A
@@ -109,7 +109,7 @@
 El-irr : {A : HOD} → {x y : Element A } → elm x ≡ elm y → x ≡ y
 El-irr {A} {x} {y} eq = El-irr2 A eq ( is-elm-irr A eq ) 
 
-record ZChain ( A : HOD ) (y : Ordinal)   : Set (suc n) where
+record ZChain ( A : HOD ) (y : Ordinal)   : Set (Level.suc n) where
    field
       max : HOD
       A∋max : A ∋ max
@@ -148,24 +148,59 @@
 IChainSet {A} ax = record { od = record { def = λ y → odef A y ∧ IChained A (& (elm ax)) y }
     ; odmax = & A ; <odmax = λ {y} lt → subst (λ k → k o< & A) &iso (c<→o< (subst (λ k → odef A k) (sym &iso) (proj1 lt))) } 
 
+open import Data.Nat hiding (_<_) 
+import Data.Nat.Properties as NP
+open import nat
+
+--   x < ... < y
+--   x < ... < y  ... < z
+
+iclen : (A : HOD) → {y : Ordinal} → IChain A y → ℕ
+iclen A {y} (ifirst x) = zero
+iclen A {y} (inext {ox} x x₁ ic) = suc ( iclen A {ox} ic )
+
+ic-1 : (A : HOD) → {x y1 y : Ordinal} → (cy : IChain A y ) → { ay1 : odef A y1 } → { y<y1 : * y < * y1 }
+     → ic-connect x (inext {A} {y} {y1} ay1 y<y1 cy) → (x ≡ y ) ∨ ic-connect x cy
+ic-1 A {x} {y1} {.x} cy {ay1} {y<y1} (case1 refl) = case1 refl
+ic-1 A {x} {y1} {y} cy {ay1} {y<y1} (case2 icy) = case2 icy
+
+ic-0 : (A : HOD) → {s x y : Ordinal} → {cx : IChain A x } {cy : IChain A y }
+    → ic-connect s cx → ¬ ic-connect x cy → ¬ ic-connect s cy
+ic-0 = {!!}
+
+ic-∨ : (A : HOD) → {s x y : Ordinal} → {cx : IChain A x } {cy : IChain A y }
+    → ic-connect s cx → ic-connect s cy
+    → ic-connect x cy ∨ ic-connect y cx
+ic-∨ = {!!}
+
+iclen-monotonic : (A : HOD) → IsPartialOrderSet A → {s x y : Ordinal} → {cx : IChain A x } {cy : IChain A y }
+    → ic-connect s cx → ic-connect s cy
+    → iclen A cx Data.Nat.≤ iclen A cy → (x ≡ y) ∨ ( (* x) < (* y) )
+iclen-monotonic A PO {s} {x} {y} {cx} {inext x₁ x₂ cy} ix (case1 s=ox ) le = {!!}
+iclen-monotonic A PO {s} {x} {y} {inext {ox} {x} x₃ x₄ cx} {inext {oy} {y} x₁ x₂ cy} ix (case2 icy) (s≤s le) = ic02 where
+     ic02 : (x ≡ y) ∨ (* x < * y)
+     ic02 with NP.<-cmp (iclen A (inext x₃ x₄ cx)) (suc ( iclen A cy ))
+     ... | tri< a ¬b ¬c =  ic03 where
+        ic01 : (x ≡ oy) ∨ ( (* x) < (* oy ))
+        ic01 = iclen-monotonic A PO {s} {x} {oy} {inext x₃ x₄ cx} {cy} ix icy {!!}
+        ic03 : (x ≡ y) ∨ ( (* x) < (* y ))
+        ic03 with ic01
+        ... | case1 x=oy = {!!}
+        ... | case2 x<oy =  case2 ( IsStrictPartialOrder.trans PO {!!} {!!} )
+     ... | tri≈ ¬a b ¬c = case2 ( subst (λ k → * k < * y) {!!} x₂ ) -- suc (iclen A cx) ≡ suc (iclen A cy) → → oy ≡ x
+     ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s le) c )
+
 IC-is-total : {A : HOD} → (ax : Element A ) → IsPartialOrderSet A → IsTotalOrderSet (IChainSet {A} ax)
 IC-is-total {A} ax PO = record { isEquivalence = IsStrictPartialOrder.isEquivalence IPO
    ; trans = λ {x} {y} {z} → IsStrictPartialOrder.trans IPO {x} {y} {z}  ; compare = cmp } where
     IPO : IsPartialOrderSet (IChainSet {A} ax)
     IPO = ⊆-IsPartialOrderSet record { incl = λ {x} lt → proj1 lt } PO
     cmp : Trichotomous _ _ 
-    cmp x y with IChained.iy (proj2 (is-elm x)) | IChained.iy (proj2 (is-elm y))
-    ... | ifirst x₁ | ifirst x₂ = tri≈ {!!} {!!} {!!} 
-    ... | ifirst x₁ | inext x₂ x₃ s = {!!}
-    ... | inext x₁ x₂ t | ifirst x₃ = {!!}
-    ... | inext x₁ x₂ t | inext x₃ x₄ s with cmp (me ⟪ subst (λ k → odef A k) (sym &iso) (ic→odef t) ,
-      record { iy = subst (λ k → IChain A k) (sym &iso) t ; ic = ic1 } ⟫) (me ⟪ subst (λ k → odef A k) (sym &iso) (ic→odef s) ,
-      record { iy = subst (λ k → IChain A k) (sym &iso) s ; ic = ic2 } ⟫) where 
-        ic1 :  ic-connect (& (elm ax)) (subst (λ k → IChain A k) (sym &iso) t)
-        ic1 = {!!}
-        ic2 :  ic-connect (& (elm ax)) (subst (λ k → IChain A k) (sym &iso) s)
-        ic2 = {!!}
-    ... | t = {!!}
+    cmp x y with iclen A (IChained.iy (proj2 (is-elm x))) | iclen A (IChained.iy (proj2 (is-elm y)))
+    ... | zero | zero = {!!}
+    ... | zero | suc t = {!!}
+    ... | suc s | zero = {!!}
+    ... | suc s | suc t = {!!}
 -- there is a y, & y > & x
 
 record OSup> (A : HOD) {x : Ordinal} (ax : A ∋ * x) : Set n where
@@ -193,7 +228,7 @@
       icy : odef (IChainSet {A} (me ax)) y  
       c-finite : ¬ IChainSup> A ax
       
-record Maximal ( A : HOD )  : Set (suc n) where
+record Maximal ( A : HOD )  : Set (Level.suc n) where
    field
       maximal : HOD
       A∋maximal : A ∋ maximal
@@ -246,7 +281,7 @@
     ... | yes inifite = case2 (case2 record {  chain<x = {!!} ;  c-infinite = {!!}  } )
 
 
-record SUP ( A B : HOD )  : Set (suc n) where
+record SUP ( A B : HOD )  : Set (Level.suc n) where
    field
       sup : HOD
       A∋maximal : A ∋ sup