# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562426341 -32400
# Node ID 35ce91192cf499057cb4421126b2baa08853e245
# Parent  327d49c2478bec9bd710076c8308565987fd4c37
replacement in ordinal-definable

diff -r 327d49c2478b -r 35ce91192cf4 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat Jul 06 18:31:46 2019 +0900
+++ b/ordinal-definable.agda	Sun Jul 07 00:19:01 2019 +0900
@@ -278,8 +278,8 @@
 csuc :  {n : Level} →  OD {suc n} → OD {suc n}
 csuc x = Ord ( osuc ( od→ord x ))
 
-f-rel : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n}
-f-rel {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → def X y → ¬ ( x ≡ od→ord (ψ (Ord y ))))  }
+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 )
 
@@ -314,10 +314,10 @@
     Select X ψ = record { def = λ x →  ((y : Ordinal {suc n}) → def X y → ψ ( ord→od y )) ∧ def X x  } 
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
-    _∩_ : ( A B : OD  ) → OD
+    _∩_ : ( A B : OD {suc n} ) → OD
     A ∩ B = record { def = λ x → def A x  ∧ def B x }
     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 (ψ (X ∩ (ord→od x ))))) ∧ def (f-rel X ψ) x }
+    Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
     Union : OD {suc n} → OD {suc n}
     Union U = record { def = λ y → osuc y o< (od→ord U) }
     -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x →  X ∋ x )
@@ -416,9 +416,11 @@
                lemma : (cond : ((y : OD) → X ∋ y → ψ y ) ∧ (X ∋ y) ) → ψ y
                lemma cond = (proj1 cond) y (proj2 cond)
          replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  sup-o< {suc n} {λ x → od→ord (ψ (ord→od x)) }  ; proj2 = {!!} }
-         replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → {y : OD} → ¬ (¬ (ψ x == y))
-         replacement→ {ψ} 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 oiso)} ) )
+         replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (ψ x == y))
+         replacement→ {ψ} X x lt not = ⊥-elim ( not (ψ x) (ord→== refl ) )
          ∅-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} 
diff -r 327d49c2478b -r 35ce91192cf4 zf.agda
--- a/zf.agda	Sat Jul 06 18:31:46 2019 +0900
+++ b/zf.agda	Sun Jul 07 00:19:01 2019 +0900
@@ -78,7 +78,7 @@
      selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  Set m } → ∀ {  y : ZFSet  } →  (((y : ZFSet) → y ∈ X → ψ y ) ∧ ( y ∈ X ) ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ 
-     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ∀ {y : ZFSet}  → ¬ ( ¬ ( ψ x ≈ y ) )
+     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( ψ x ≈ y ) )
    -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
    -- axiom-of-choice : Set (suc n) 
    -- axiom-of-choice = ?