# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559967490 -32400
# Node ID 4659a815b70d915773bcc364627f00bfd8032f81
# Parent  d382a7902f5e4f0cffb3ee74bd47d10c7ada59bb
...

diff -r d382a7902f5e -r 4659a815b70d ordinal-definable.agda
--- a/ordinal-definable.agda	Thu Jun 06 09:36:41 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 08 13:18:10 2019 +0900
@@ -136,21 +136,12 @@
 o≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  ord→od x == ord→od y
 o≡→== {n} {x} {.x} refl = eq-refl
 
-
-=→¬< : {x : Nat  } → ¬ ( x < x )
-=→¬< {Zero} ()
-=→¬< {Suc x} (s≤s lt) = =→¬< lt
-
 >→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
 
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
-o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy  → ox o< oy  → ⊥
-o<¬≡ ox ox refl (case1 lt) =  =→¬< lt
-o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
-
 o<→o> : {n : Level} →  { x y : OD {n} } →  (x == y) → (od→ord x ) o< ( od→ord y) → ⊥
 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with
      yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case1 lt )) oiso diso )
@@ -188,10 +179,6 @@
          t : def (ord→od (od→ord a)) (od→ord (ord→od (od→ord x)))
          t = o<→c< {suc n} {od→ord x} {od→ord a} lt 
 
-¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
-¬x<0 {n} {x} (case1 ())
-¬x<0 {n} {x} (case2 ())
-
 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
@@ -256,8 +243,10 @@
      lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (∅5 ¬p))  
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
-postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
+Def : OD {suc n} → OD {suc n}
+Def X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x  }
 
 
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
@@ -284,7 +273,7 @@
     Union U = record { def = λ y → osuc y o< (od→ord U) }
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
     Power : OD {suc n} → OD {suc n}
-    Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x  }
+    Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def (ord→od y) x  → def X x }
     ZFSet = OD {suc n}
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
@@ -322,11 +311,11 @@
          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  }
+         --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x  →  def X x }
          power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ A t P∋t {x} t∋x = {!!}
+         power→ A t P∋t {x} t∋x = ?
          power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A z = {!!}
+         power← A t t→A z _ = ?
          union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
          union-u X z U>z = ord→od ( osuc ( od→ord z ) )
          union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z  ∋ z
diff -r d382a7902f5e -r 4659a815b70d ordinal.agda
--- a/ordinal.agda	Thu Jun 06 09:36:41 2019 +0900
+++ b/ordinal.agda	Sat Jun 08 13:18:10 2019 +0900
@@ -109,6 +109,18 @@
 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
 ¬a≤a  (s≤s lt) = ¬a≤a  lt
 
+=→¬< : {x : Nat  } → ¬ ( x < x )
+=→¬< {Zero} ()
+=→¬< {Suc x} (s≤s lt) = =→¬< lt
+
+o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy  → ox o< oy  → ⊥
+o<¬≡ ox ox refl (case1 lt) =  =→¬< lt
+o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
+
+¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
+¬x<0 {n} {x} (case1 ())
+¬x<0 {n} {x} (case2 ())
+
 o<> : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
 o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<>  x₁ x₂
 o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁