# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563784312 -32400
# Node ID 65e1b2e415bb8e4287ce452e8d59addb3fc3abf8
# Parent  de3d87b7494fe4bfa21265cdaff38b12dee8b8e6
...

diff -r de3d87b7494f -r 65e1b2e415bb OD.agda
--- a/OD.agda	Sun Jul 21 17:56:12 2019 +0900
+++ b/OD.agda	Mon Jul 22 17:31:52 2019 +0900
@@ -525,3 +525,22 @@
                                lx ≡ ly → ly ≡ lv (od→ord z)  → ψ z 
                           lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
 
+         ==→o≡' : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
+         ==→o≡' {n} {x} {y} eq = lemma1 {!!}  where
+            lemma4 : { x y : OD {suc n} } → (x == y) →  ¬ ( od→ord x o< od→ord y  )
+            lemma4 = {!!}
+            lemma3 : { x y : OD {suc n} } → (x == y) →  od→ord x ≡ od→ord y 
+            --       x  <   y
+            --    m     m 
+            lemma3 {x} {y} eq with trio< (od→ord x) (od→ord y)
+            lemma3 {x} {y} eq | tri≈ ¬a b ¬c = b
+            lemma3 {x} {y} eq | tri< a ¬b ¬c = {!!}
+            lemma3 {x} {y} eq | tri> ¬a ¬b c = {!!} 
+            lemma1 : { x y : OD {suc n} } → Ord (od→ord x) == Ord (od→ord y)  → x ≡ y
+            lemma1 {x} {y} eq = subst₂ (λ k j → k ≡ j ) oiso oiso (cong (λ k → ord→od k ) lemma2) where
+                 lemma2 : (od→ord x) ≡ (od→ord y)
+                 lemma2 with trio< (od→ord x) (od→ord y)
+                 lemma2 | tri≈ ¬a b ¬c = b
+                 lemma2 | tri< a ¬b ¬c with eq← eq a
+                 ... | lt = ⊥-elim ( o<¬≡ refl lt )
+                 lemma2 | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl ( eq→ eq c ))
diff -r de3d87b7494f -r 65e1b2e415bb ordinal.agda
--- a/ordinal.agda	Sun Jul 21 17:56:12 2019 +0900
+++ b/ordinal.agda	Mon Jul 22 17:31:52 2019 +0900
@@ -17,9 +17,6 @@
      lv : Nat
      ord : OrdinalD {n} lv
 
---
---    Φ (Suc lv) < ℵ lv < OSuc (Suc lv) (ℵ lv) < OSuc ... < OSuc (Suc lv) (Φ (Suc lv)) < OSuc ...  < ℵ (Suc lv)
---
 data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
    Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
    s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
@@ -300,8 +297,6 @@
 proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt
 ... | refl = case2 (s< lt)
 
--- omax≡ (omax x x ) (osuc x) (omxx x)
-
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
 OrdTrans (case1 refl) (case1 refl) = case1 refl
 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
@@ -327,7 +322,7 @@
 TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = 
       caseOSuc lx ox (TransFinite caseΦ caseOSuc  record { lv = lx ; ord = ox })
 
--- we cannot prove this in intutonistic logic 
+-- we cannot prove this in intutionistic logic 
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
 -- postulate 
 --  TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )