--- 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} {!!} ) {!!} {!!}