changeset 141:21b2654985c4

fix or
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2019 00:20:30 +0900
parents 312e27aa3cb5
children c30bc9f5bd0d
files HOD.agda ordinal-definable.agda
diffstat 2 files changed, 115 insertions(+), 95 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Sun Jul 07 23:02:47 2019 +0900
+++ b/HOD.agda	Mon Jul 08 00:20:30 2019 +0900
@@ -13,17 +13,17 @@
 
 -- Ordinal Definable Set
 
-record HOD {n : Level}  : Set (suc n) where
+record OD {n : Level}  : Set (suc n) where
   field
     def : (x : Ordinal {n} ) → Set n
 
-open HOD
+open OD
 open import Data.Unit
 
 open Ordinal
 open _∧_
 
-record _==_ {n : Level} ( a b :  HOD {n} ) : Set n where
+record _==_ {n : Level} ( a b :  OD {n} ) : Set n where
   field
      eq→ : ∀ { x : Ordinal {n} } → def a x → def b x 
      eq← : ∀ { x : Ordinal {n} } → def b x → def a x 
@@ -31,37 +31,37 @@
 id : {n : Level} {A : Set n} → A → A
 id x = x
 
-eq-refl : {n : Level} {  x :  HOD {n} } → x == x
+eq-refl : {n : Level} {  x :  OD {n} } → x == x
 eq-refl {n} {x} = record { eq→ = id ; eq← = id }
 
 open  _==_ 
 
-eq-sym : {n : Level} {  x y :  HOD {n} } → x == y → y == x
+eq-sym : {n : Level} {  x y :  OD {n} } → x == y → y == x
 eq-sym eq = record { eq→ = eq← eq ; eq← = eq→ eq }
 
-eq-trans : {n : Level} {  x y z :  HOD {n} } → x == y → y == z → x == z
+eq-trans : {n : Level} {  x y z :  OD {n} } → x == y → y == z → x == z
 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y  t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
 
-⇔→== : {n : Level} {  x y :  HOD {suc n} } → ( {z : Ordinal {suc n}} → def x z ⇔  def y z) → x == y 
+⇔→== : {n : Level} {  x y :  OD {suc n} } → ( {z : Ordinal {suc n}} → def x z ⇔  def y z) → x == y 
 eq→ ( ⇔→== {n} {x} {y}  eq ) {z} m = proj1 eq m 
 eq← ( ⇔→== {n} {x} {y}  eq ) {z} m = proj2 eq m 
 
--- Ordinal in HOD ( and ZFSet )
-Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n}
+-- Ordinal in OD ( and ZFSet )
+Ord : { n : Level } → ( a : Ordinal {n} ) → OD {n}
 Ord {n} a = record { def = λ y → y o< a }  
 
-od∅ : {n : Level} → HOD {n} 
+od∅ : {n : Level} → OD {n} 
 od∅ {n} = Ord o∅ 
 
 postulate      
-  -- HOD can be iso to a subset of Ordinal ( by means of Godel Set )
-  od→ord : {n : Level} → HOD {n} → Ordinal {n}
-  ord→od : {n : Level} → Ordinal {n} → HOD {n} 
-  c<→o<  : {n : Level} {x y : HOD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
-  oiso   : {n : Level} {x : HOD {n}}     → ord→od ( od→ord x ) ≡ x
+  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
+  od→ord : {n : Level} → OD {n} → Ordinal {n}
+  ord→od : {n : Level} → Ordinal {n} → OD {n} 
+  c<→o<  : {n : Level} {x y : OD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
+  oiso   : {n : Level} {x : OD {n}}     → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   ord-Ord :{n : Level} {x : Ordinal {n}} →  x ≡ od→ord (Ord x)   
-  ==→o≡ : {n : Level} →  { x y : HOD {suc n} } → (x == y) → x ≡ y
+  ==→o≡ : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
   -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
   -- supermum as Replacement Axiom
@@ -71,38 +71,38 @@
   sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
-  minimul : {n : Level } → (x : HOD {suc n} ) → ¬ (x == od∅ )→ HOD {suc n} 
+  minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
   -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
-  x∋minimul : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
-  minimul-1 : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+  x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
+  minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
   -- we should prove this in agda, but simply put here
-  ===-≡ : {n : Level} { x y : HOD {suc n}} → x == y  → x ≡ y
+  ===-≡ : {n : Level} { x y : OD {suc n}} → x == y  → x ≡ y
 
 Ord-ord : {n : Level } {ox : Ordinal {suc n}} → Ord ox ≡ ord→od ox
 Ord-ord {n} {px} = trans (sym oiso) (cong ( λ k → ord→od k ) (sym ord-Ord)) 
 
-_∋_ : { n : Level } → ( a x : HOD {n} ) → Set n
+_∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
-_c<_ : { n : Level } → ( x a : HOD {n} ) → Set n
+_c<_ : { n : Level } → ( x a : OD {n} ) → Set n
 x c< a = a ∋ x 
 
-_c≤_ : {n : Level} →  HOD {n} →  HOD {n} → Set (suc n)
+_c≤_ : {n : Level} →  OD {n} →  OD {n} → Set (suc n)
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
 
-cseq : {n : Level} →  HOD {n} →  HOD {n}
+cseq : {n : Level} →  OD {n} →  OD {n}
 cseq x = record { def = λ y → def x (osuc y) } where
 
-def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
+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
 
 o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x 
 o<→c< {n} {x} {y} lt = subst ( λ k → k o< y ) ord-Ord lt 
 
-sup-od : {n : Level } → ( HOD {n} → HOD {n}) →  HOD {n}
+sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
 sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
 
-sup-c< : {n : Level } → ( ψ : HOD {n} →  HOD {n}) → ∀ {x : HOD {n}} → def ( sup-od ψ ) (od→ord ( ψ x ))
+sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x ))
 sup-c< {n} ψ {x} = def-subst {n} {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
         lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
     lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
@@ -149,21 +149,21 @@
 ord-iso = cong ( λ k → record { lv = lv k ; ord = ord k } ) diso
 
 -- avoiding lv != Zero error
-orefl : {n : Level} →  { x : HOD {n} } → { y : Ordinal {n} } → od→ord x ≡ y → od→ord x ≡ y
+orefl : {n : Level} →  { x : OD {n} } → { y : Ordinal {n} } → od→ord x ≡ y → od→ord x ≡ y
 orefl refl = refl
 
-==-iso : {n : Level} →  { x y : HOD {n} } → ord→od (od→ord x) == ord→od (od→ord y)  →  x == y
+==-iso : {n : Level} →  { x y : OD {n} } → ord→od (od→ord x) == ord→od (od→ord y)  →  x == y
 ==-iso {n} {x} {y} eq = record {
       eq→ = λ d →  lemma ( eq→  eq (def-subst d (sym oiso) refl )) ;
       eq← = λ d →  lemma ( eq←  eq (def-subst d (sym oiso) refl ))  }
         where
-           lemma : {x : HOD {n} } {z : Ordinal {n}} → def (ord→od (od→ord x)) z → def x z
+           lemma : {x : OD {n} } {z : Ordinal {n}} → def (ord→od (od→ord x)) z → def x z
            lemma {x} {z} d = def-subst d oiso refl
 
-=-iso : {n : Level } {x y : HOD {suc n} } → (x == y) ≡ (ord→od (od→ord x) == y)
+=-iso : {n : Level } {x y : OD {suc n} } → (x == y) ≡ (ord→od (od→ord x) == y)
 =-iso {_} {_} {y} = cong ( λ k → k == y ) (sym oiso)
 
-ord→== : {n : Level} →  { x y : HOD {n} } → od→ord x ≡  od→ord y →  x == y
+ord→== : {n : Level} →  { x y : OD {n} } → od→ord x ≡  od→ord y →  x == y
 ord→== {n} {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
    lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
    lemma ox ox  refl = eq-refl
@@ -174,10 +174,10 @@
 >→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
 
-c≤-refl : {n : Level} →  ( x : HOD {n} ) → x c≤ x
+c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
-∋→o< : {n : Level} →  { a x : HOD {suc n} } → a ∋ x → od→ord x o< od→ord a
+∋→o< : {n : Level} →  { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
 ∋→o< {n} {a} {x} lt = t where
          t : (od→ord x) o< (od→ord a)
          t = c<→o< {suc n} {x} {a} lt 
@@ -191,10 +191,10 @@
 o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
 o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 
-o<→¬c> : {n : Level} →  { x y : HOD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
+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<> olt (c<→o< clt ) where
 
-o≡→¬c< : {n : Level} →  { x y : HOD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
+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<¬≡  (orefl oeq ) (c<→o< lt) 
 
 ∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ } == od∅ {n} 
@@ -202,14 +202,14 @@
 eq← ∅0 {w} (case1 ())
 eq← ∅0 {w} (case2 ())
 
-∅< : {n : Level} →  { x y : HOD {n} } → def x (od→ord y ) → ¬ (  x  == od∅ {n} )
+∅< : {n : Level} →  { x y : OD {n} } → def x (od→ord y ) → ¬ (  x  == od∅ {n} )
 ∅< {n} {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
 ∅< {n} {x} {y} d eq | lift ()
        
-∅6 : {n : Level} →  { x : HOD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
+∅6 : {n : Level} →  { x : OD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
 ∅6 {n} {x} x∋x = o<¬≡ refl ( c<→o< {suc n} {x} {x} x∋x )
 
-def-iso : {n : Level} {A B : HOD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
+def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
 def-iso refl t = t
 
 is-o∅ : {n : Level} →  ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} )
@@ -221,15 +221,18 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
 
-csuc :  {n : Level} →  HOD {suc n} → HOD {suc n}
+csuc :  {n : Level} →  OD {suc n} → OD {suc n}
 csuc x = Ord ( osuc ( od→ord x ))
 
+in-codomain : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n}
+in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))  }
+
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
-ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
+ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }   where
 
-Def :  {n : Level} → (A :  HOD {suc n}) → HOD {suc n}
+Def :  {n : Level} → (A :  OD {suc n}) → OD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
 OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
@@ -250,7 +253,7 @@
 -- L (Φ 0) = Φ
 -- L (OSuc lv n) = { Def ( L n )  } 
 -- L (Φ (Suc n)) = Union (L α) (α < Φ (Suc n) )
-L : {n : Level} → (α : Ordinal {suc n}) → HOD {suc n}
+L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
 L {n}  record { lv = Zero ; ord = (Φ .0) } = od∅
 L {n}  record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
@@ -265,14 +268,14 @@
       lemma0 {n} ox = trans (cong (λ k → od→ord k) (===-≡ (⇔→== lemma1) )) (sym ord-Ord)
 
 -- L0 :  {n : Level} → (α : Ordinal {suc n}) → α o< β → L (osuc α) ∋ L α
--- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : HOD {suc n})  → L α ∋ x → L β ∋ x 
+-- L1 :  {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n})  → L α ∋ x → L β ∋ x 
 
 omega : { n : Level } → Ordinal {n}
 omega = record { lv = Suc Zero ; ord = Φ 1 }
 
-HOD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
-HOD→ZF {n}  = record { 
-    ZFSet = HOD {suc n}
+OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
+OD→ZF {n}  = record { 
+    ZFSet = OD {suc n}
     ; _∋_ = _∋_ 
     ; _≈_ = _==_ 
     ; ∅  = od∅
@@ -284,23 +287,23 @@
     ; infinite = Ord omega
     ; isZF = isZF 
  } where
-    Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
+    Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → Set (suc n) ) → OD {suc n}
     Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) }
-    Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-    Replace X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧  ( x == ψ (Ord y)  ))))
-    _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
+    Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
+    Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+    _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
-    Union : HOD {suc n} → HOD {suc n}
+    Union : OD {suc n} → OD {suc n}
     Union U = cseq U 
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
-    ZFSet = HOD {suc n}
+    ZFSet = OD {suc n}
     _∈_ : ( A B : ZFSet  ) → Set (suc n)
     A ∈ B = B ∋ A
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
     _∩_ : ( A B : ZFSet  ) → ZFSet
     A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
-    Power : HOD {suc n} → HOD {suc n}
+    Power : OD {suc n} → OD {suc n}
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
     -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
@@ -310,7 +313,7 @@
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (HOD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (Ord omega)
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (Ord omega)
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -330,11 +333,11 @@
        ;   replacement→ = replacement→
      } where
 
-         pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
+         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)
 
-         empty : (x : HOD {suc n} ) → ¬  (od∅ ∋ x)
+         empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x (case1 ())
          empty x (case2 ())
 
@@ -346,18 +349,18 @@
          --    then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x
          --    In case of later, ZFSubset A ∋ t and t ∋ x implies A ∋ x by transitivity
          --
-         POrd : {a : Ordinal } {t : HOD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
+         POrd : {a : Ordinal } {t : OD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
          POrd {a} {t} P∋t = o<→c< P∋t
-         ord-power→ : (a : Ordinal ) ( t : HOD) → Def (Ord a) ∋ t → {x : HOD} → t ∋ x → Ord a ∋ x
+         ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → t ∋ x → Ord a ∋ x
          ord-power→ a t P∋t {x} t∋x with osuc-≡<  (sup-lb  (POrd P∋t))
          ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )  where
-              Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
+              Ltx :   {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
          ... | case2 lt = {!!} where
               sp =  sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
-              minsup :  HOD
+              minsup :  OD
               minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
-              Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
+              Ltx :   {n : Level} → {x t : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
               -- lemma1 hold because minsup is Ord (minα a sp) 
               lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
@@ -380,7 +383,7 @@
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
          -- 
-         ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
+         ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
          ord-power← a t t→A  = def-subst {suc n} {_} {_} {Def (Ord a)} {od→ord t}
                  lemma refl (lemma1 lemma-eq )where
               lemma-eq :  ZFSubset (Ord a) t == t
@@ -388,48 +391,59 @@
               eq← lemma-eq {z} w = record { proj2 = w  ;
                  proj1 = def-subst {suc n} {_} {_} {(Ord a)} {z}
                     ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
-              lemma1 : {n : Level } {a : Ordinal {suc n}} { t : HOD {suc n}}
+              lemma1 : {n : Level } {a : Ordinal {suc n}} { t : OD {suc n}}
                  → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
               lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
               lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o<   
 
          -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
-         power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
+         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
          power→ = {!!}
-         power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+         power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
          power← A t t→A = {!!} where 
               a = od→ord A
-              ψ : HOD → HOD
+              ψ : OD → OD
               ψ y = Def (Ord a) ∩ y
 
-         union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
+         union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
-         union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
          union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
          union→ X z u xx | tri< a ¬b ¬c | ()
          union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b 
          union→ X z u xx | tri> ¬a ¬b c = {!!}
-         union← :  (X z : HOD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
+         union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
          union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
              lemma : X ∋ union-u {X} {z} X∋z
              lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord
 
-         -- ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
-         -- ψiso {ψ} t refl = t
-         selection : {ψ : HOD → Set (suc n)} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-         selection {X} {ψ} {y} = {!!}
-         replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = {!!}
-         replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma {!!} where
-            lemma :  ( (y : HOD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
-            lemma not y not2 = not (ord→od y) (subst₂ ( λ k j → k == j ) oiso (cong (λ k → ψ k ) Ord-ord ) (proj2 not2 ))
+         ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
+         ψiso {ψ} t refl = t
+         selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+         selection {ψ} {X} {y} = record {
+              proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
+            ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
+           }
+         replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
+         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
+             lemma : def (in-codomain X ψ) (od→ord (ψ x))
+             lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
+                 (sym (subst (λ k → Ord (od→ord x) ≡ k) oiso (Ord-ord) )) } ))
+         replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
+         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+            lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
+                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
+            lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
+                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))  
+                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
+            lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
+            lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso  ( proj2 not2 ))
 
-         ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
+         ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
-         regularity :  (x : HOD) (not : ¬ (x == od∅)) →
+         regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = x∋minimul x not
          proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where
@@ -440,12 +454,12 @@
              lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
              lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
 
-         extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+         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  
 
          open  import  Relation.Binary.PropositionalEquality
-         uxxx-ord : {x  : HOD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
+         uxxx-ord : {x  : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
          uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x))  where
               lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 
               lemma {y} = let open ≡-Reasoning in begin
@@ -459,11 +473,11 @@
                 ≡⟨ cong (λ k → osuc y o<  k ) (omxxx  (od→ord x) )  ⟩
                    osuc y o< osuc (osuc (od→ord x))

-         infinite : HOD {suc n}
+         infinite : OD {suc n}
          infinite = Ord omega 
          infinity∅ : Ord omega  ∋ od∅ {suc n}
          infinity∅ = o<-subst (case1 (s≤s z≤n) ) ord-Ord refl
-         infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
+         infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
          infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where
               eq :  osuc (od→ord x) ≡ od→ord (Union (x , (x , x)))
               eq = let open ≡-Reasoning in begin
@@ -482,12 +496,12 @@
               lemma record { lv = (Suc Zero) ; ord = (Φ .1) } (case2 ()) | refl
          -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] -- this form is no good since X is a transitive set
          -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ { t }) ]
-         record Choice (z : HOD {suc n}) : Set (suc (suc n)) where
+         record Choice (z : OD {suc n}) : Set (suc (suc n)) where
              field
-                 u : {x : HOD {suc n}} ( x∈z  : x ∈ z ) → HOD {suc n}
-                 t : {x : HOD {suc n}} ( x∈z  : x ∈ z ) → (x : HOD {suc n} ) → HOD {suc n}
-                 choice : { x : HOD {suc n} } → ( x∈z  : x ∈ z ) → ( u x∈z ∩ x) == { t x∈z x }
-         -- choice : {x :  HOD {suc n}} ( x ∈ z  → ¬ ( x ≈ ∅ ) ) →
-         -- axiom-of-choice : { X : HOD } → ( ¬x∅ : ¬ ( X == od∅ ) ) → { A : HOD } → (A∈X : A ∈ X ) →  choice ¬x∅ A∈X ∈ A 
+                 u : {x : OD {suc n}} ( x∈z  : x ∈ z ) → OD {suc n}
+                 t : {x : OD {suc n}} ( x∈z  : x ∈ z ) → (x : OD {suc n} ) → OD {suc n}
+                 choice : { x : OD {suc n} } → ( x∈z  : x ∈ z ) → ( u x∈z ∩ x) == { t x∈z x }
+         -- choice : {x :  OD {suc n}} ( x ∈ z  → ¬ ( x ≈ ∅ ) ) →
+         -- axiom-of-choice : { X : OD } → ( ¬x∅ : ¬ ( X == od∅ ) ) → { A : OD } → (A∈X : A ∈ X ) →  choice ¬x∅ A∈X ∈ A 
          -- axiom-of-choice {X} nx {A} lt = ¬∅=→∅∈ {!!}
 
--- a/ordinal-definable.agda	Sun Jul 07 23:02:47 2019 +0900
+++ b/ordinal-definable.agda	Mon Jul 08 00:20:30 2019 +0900
@@ -418,7 +418,14 @@
              lemma : def (in-codomain X ψ) (od→ord (ψ x))
              lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ) )
          replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!}) )
+         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+            lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
+                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
+            lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
+                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))  
+                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
+            lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
+            lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso  ( proj2 not2 ))
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
@@ -431,8 +438,7 @@
             lemma (case1 ())
             lemma (case2 ())
             reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
-            reg {y} t with {!!}
-            ... | x∈∅ = o<-subst (proj1 x∈∅) diso refl
+            reg {y} t = ⊥-elim ( ¬x<0 (proj1 (proj2 t )) )
          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