# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559685948 -32400
# Node ID 296388c033589e10f2b246e857f59ecd178fc6c9
# Parent  08be6351927ef9c1845fe285e06311f514f66a77
split omax?

diff -r 08be6351927e -r 296388c03358 ordinal-definable.agda
--- a/ordinal-definable.agda	Wed Jun 05 03:21:47 2019 +0900
+++ b/ordinal-definable.agda	Wed Jun 05 07:05:48 2019 +0900
@@ -293,8 +293,8 @@
          open _∧_ 
          open Minimumo
          pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
-         proj1 (pair A B ) = omax-x {n} {od→ord A} {od→ord B}
-         proj2 (pair A B ) = omax-y {n} {od→ord A} {od→ord B}
+         proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
+         proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
          --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x )  }
@@ -344,7 +344,7 @@
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
          pair-osuc : {x y : OD {suc n}} →  (x , x)  ∋ y →  (od→ord y ) o< osuc (od→ord x) 
-         pair-osuc {x} {y} z with union← (x , x) y z
+         pair-osuc {x} {y} z with union← (x , x) y {!!}
          ... | t = {!!}
          next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
          eq→ (next x ) {y} z = {!!}       --   z : y o< osuc (osuc ox ) → y < osuc ox
@@ -353,7 +353,7 @@
              lemma0 :  (x , x) ∋ ord→od y 
              lemma0 = o<-subst {suc n} {od→ord (ord→od y)} {od→ord {!!}} (c<→o< z) {!!} {!!}
              lemma1 : (x , (x , x)) ∋ ord→od (osuc y)    -- z : def (ord→od (osuc (od→ord x))) y
-             lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< z) oiso refl)
+             lemma1 with osuc-≡< {suc n} (def-subst {suc n} (o<→c< {!!}) oiso refl)
              lemma1 | case1 x = {!!}
              lemma1 | case2 t = {!!}
              -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!}
diff -r 08be6351927e -r 296388c03358 ordinal.agda
--- a/ordinal.agda	Wed Jun 05 03:21:47 2019 +0900
+++ b/ordinal.agda	Wed Jun 05 07:05:48 2019 +0900
@@ -240,23 +240,18 @@
 omax-y {n} x y | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = <-osuc
 omax-y {n} x y | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ordtrans (case2 c) <-osuc
 
-omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
-omxx {n} x with <-cmp (lv x) (lv x)
-omxx {n} x | tri< a ¬b ¬c = refl
-omxx {n} x | tri> ¬a ¬b c = refl
-omxx {n} x | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord x)
-omxx {n} x | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl
-omxx {n} x | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
-omxx {n} x | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = refl
+-- omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
+-- omxx {n} record { lv = Zero ; ord = (Φ .0) } = refl
+-- omxx {n} record { lv = Zero ; ord = (OSuc .0 (Φ .0)) } = refl
+-- omxx {n} record { lv = Zero ; ord = (OSuc .0 (OSuc .0 ord₁)) } = ?
+-- omxx {n} record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } = {!!}
+-- omxx {n} record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } = {!!}
 
 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
 omxxx {n} x with <-cmp (lv x) (lv x)
-omxxx {n} x | tri< a ¬b ¬c = refl
-omxxx {n} x | tri> ¬a ¬b c = refl
-omxxx {n} x | tri≈ ¬a refl ¬c with triOrdd (ord x) (ord x)
-omxxx {n} x | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = refl
-omxxx {n} x | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl
-omxxx {n} x | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = refl
+omxxx {n} x | tri< a ¬b ¬c = ? -- ⊥-elim (¬b refl)
+omxxx {n} x | tri> ¬a ¬b c = ? -- ⊥-elim (¬b refl) 
+omxxx {n} x | tri≈ ¬a refl ¬c = ?
 
 
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_