--- a/ordinal-definable.agda	Mon Jun 03 12:29:33 2019 +0900
+++ b/ordinal-definable.agda	Tue Jun 04 01:05:33 2019 +0900
@@ -73,13 +73,9 @@
 ∅1 {n} x (lift ())
 
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
-∅3 {n} {x} = TransFinite {n} c1 c2 c3 x where
+∅3 {n} {x} = TransFinite {n} c2 c3 x where
    c0 : Nat →  Ordinal {n}  → Set n
    c0 lx x = (∀(y : Ordinal {n}) → ¬ (y o< x))  → x ≡ o∅ {n}
-   c1 : ∀ (lx : Nat ) →  c0 lx (record { lv = Suc lx ; ord = ℵ lx } )  
-   c1 lx not with not ( record { lv = lx ; ord = Φ lx } )
-   ... | t with t (case1 ≤-refl )
-   c1 lx not | t | ()
    c2 : (lx : Nat) → c0 lx (record { lv = lx ; ord = Φ lx } )
    c2 Zero not = refl
    c2 (Suc lx) not with not ( record { lv = lx ; ord = Φ lx } )
@@ -92,9 +88,6 @@
    c3 lx (OSuc .lx x₁) d not with not (  record { lv = lx ; ord = OSuc lx x₁ } )
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
-   c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) }  )
-   ... | t with t (case2 (s< ℵΦ<   )) 
-   c3 .(Suc lx) (ℵ lx) d not | t | ()
 
 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
@@ -153,15 +146,6 @@
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
-o<> : {n : Level } ( ox oy : Ordinal {n}) → ox o<  oy  → oy o< ox  →  ⊥
-o<> ox oy (case1 x<y) (case1 y<x) = >→¬< x<y y<x
-o<> ox oy (case1 x<y) (case2 y<x) with d<→lv  y<x
-... | refl = =→¬< x<y
-o<> ox oy (case2 x<y) (case1 y<x) with d<→lv  x<y
-... | refl = =→¬< y<x
-o<> ox oy (case2 x<y) (case2 y<x) with d<→lv  x<y
-... | refl = trio<> x<y y<x
-
 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
@@ -186,14 +170,6 @@
 ¬x<0 {n} {x} (case1 ())
 ¬x<0 {n} {x} (case2 ())
 
--- o∅≡od∅0 : {n : Level} → ord→od (o∅ {suc n}) == od∅ {suc n}
--- eq→ (o∅≡od∅0 {n} ) {x} y with c<→o< {suc n} {ord→od x} {ord→od (o∅ {suc n})} (def-subst {suc n} {_} {_} {ord→od o∅} {od→ord (ord→od x)} y refl (sym diso) )
--- eq→ (o∅≡od∅0 {n}) {x} y | lt = ⊥-elim ( ¬x<0 (o<-subst lt  ord-iso  diso ) )
--- eq← (o∅≡od∅0 {n}) {x} (lift ())
--- 
--- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
--- o∅≡od∅ {n} = trans (cong (λ k → ord→od k ) ( ==→o≡ {n} (eq-trans o∅≡od∅0 (subst (λ k →  od∅ == k ) (sym oiso) eq-refl )) ) ) oiso
-
 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
@@ -207,7 +183,7 @@
 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
 
 o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
-o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where
+o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
 
 o≡→¬c< : {n : Level} →  { x y : OD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
 o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) (c<→o< lt) 
@@ -270,7 +246,7 @@
     ; Power = Power
     ; Select = Select
     ; Replace = Replace
-    ; infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } )
+    ; infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
     ; isZF = isZF 
  } where
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
@@ -296,7 +272,7 @@
     infixr  200 _∈_
     infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } ))
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -368,15 +344,23 @@
          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  
          next : (x : OD) → Union (x , (x , x)) == ord→od (osuc (od→ord x))
-         eq→ (next x ) {y} z = {!!}
+         eq→ (next x ) {y} z = {!!} 
          eq← (next x ) {y} z = {!!}
+         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)
          infinite : OD {suc n}
-         infinite = ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } )
-         infinity∅ : ord→od ( record { lv = Suc Zero ; ord = ℵ Zero  } ) ∋ od∅ {suc n}
+         infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
+         infinity∅ : ord→od ( record { lv = Suc Zero ; ord = Φ 1  } ) ∋ od∅ {suc n}
          infinity∅ = def-subst {suc n} {_} {od→ord (ord→od o∅)} {infinite} {od→ord od∅}
               (o<→c< ( case1 (s≤s z≤n )))  refl (cong (λ k →  od→ord k) o∅≡od∅ )
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x ∞∋x = {!!}
+         infinity x ∞∋x = {!!} where
+             lemma : (ox : Ordinal {suc n} ) → ox o< record { lv = Suc Zero ; ord = Φ 1 } → osuc ox o< record { lv = Suc Zero ; ord = Φ 1 } 
+             lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 {!!}
+             lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 {!!}
+             lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
+             lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))
+             lemma record { lv = 1 ; ord = (Φ 1) } (case2 ℵΦ<) = case2 {!!}
          replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = {!!}