# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559695639 -32400
# Node ID dccc9e2d1804be3a6dfda0c8727015e047505a1b
# Parent  975e72ae05412093dcd0bf272a6d20ef0313e0ba
...

diff -r 975e72ae0541 -r dccc9e2d1804 ordinal-definable.agda
--- a/ordinal-definable.agda	Wed Jun 05 09:10:33 2019 +0900
+++ b/ordinal-definable.agda	Wed Jun 05 09:47:19 2019 +0900
@@ -235,6 +235,9 @@
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
+postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
+
+
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -343,24 +346,12 @@
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          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 {!!}
-         ... | 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
-         eq← (next x ) {y} z = def-subst {suc n} {_} {_} {Union (x , (x , x))} {_}
-                  (union→ (x , (x , x)) (ord→od y) (ord→od (osuc y)) (record { proj1 = lemma1 ; proj2 = lemma2 } )) refl diso where
-             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< {!!}) oiso refl)
-             lemma1 | case1 x = {!!}
-             lemma1 | case2 t = {!!}
-             -- = o<-subst (c<→o< {suc n} {_} {ord→od y} {!!} ) {!!} {!!}
-             lemma2 : ord→od (osuc y) ∋ ord→od y
-             lemma2 = o<→c< <-osuc
-         next' : (x : OD) →  ord→od ( od→ord ( Union (x , (x , x)))) == ord→od (osuc (od→ord x))
-         next' x = subst ( λ k → k == ord→od (osuc (od→ord x))) (sym oiso) (next x)
+         xx-union : {x  : OD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) }
+         xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x))
+         xxx-union : {x  : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))}
+         xxx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) lemma where
+             lemma : {x  : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
+             lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) {!!} ) ) ( cong ( λ k → osuc k ) {!!} )
          infinite : OD {suc n}
          infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
          infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1  } ) ∋ od∅ {suc n}