# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562081158 -32400
# Node ID 5dcd5a3583a069f32a315eae61c073ca0ccd9e1d
# Parent  3849614bef1890d501f96515ac2ed737bea952a1
...

diff -r 3849614bef18 -r 5dcd5a3583a0 ordinal-definable.agda
--- a/ordinal-definable.agda	Tue Jul 02 15:59:07 2019 +0900
+++ b/ordinal-definable.agda	Wed Jul 03 00:25:58 2019 +0900
@@ -307,12 +307,14 @@
     ; 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}
-    Replace X ψ = record { def = λ x → ( X ∋ ord→od x ) ∧ (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) }
     Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
     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 = 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 )))) }
     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 )
@@ -323,8 +325,6 @@
     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) )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
     -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
     infixr  200 _∈_
@@ -346,10 +346,10 @@
        ;   infinity∅ = infinity∅
        ;   infinity = λ _ → infinity
        ;   selection = λ {X} {ψ} {y} → selection {ψ} {X} {y} 
-       ;   repl-x = λ {ψ} {X} {x} lt → Ord (sup-x (λ x → od→ord (ψ (ord→od x))))
-       ;   repl-x-∈ = λ {ψ} {X} {x} lt  → {!!}
-       ;   replacement← = {!!}
-       ;   replacement→ = {!!}
+       ;   repl-x = repl-x
+       ;   repl-x-∈ = repl-x-∈
+       ;   replacement← = replacement←
+       ;   replacement→ = replacement→
      } where
          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)
@@ -414,8 +414,19 @@
            } where
                lemma : (cond : ((y : OD) → X ∋ y → ψ y ) ∧ (X ∋ y) ) → ψ y
                lemma cond = (proj1 cond) y (proj2 cond)
-         replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
-         replacement {ψ} X x = {!!} -- sup-c< ψ {x}
+         repl-x  : {ψ : OD → OD} {X x : OD} → (lt : Replace X ψ ∋ x) → OD
+         repl-x {ψ} {X} {x} lt = Ord (sup-x (λ x → od→ord (ψ (ord→od x))))
+         repl-x-∈  : {ψ : OD → OD} {X x : OD} → (lt : Replace X ψ ∋ x) → X ∋ repl-x {ψ} {X} {x} lt
+         repl-x-∈ {ψ} {X} {x} lt = {!!}
+         X∩x : {X x : OD} →  X ∋ x → X ∩ x ≡ x
+         X∩x = {!!}
+         replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
+         replacement← {ψ} X x lt = def-subst  ( sup-c< ψ {x} ) (sym lemma) refl where
+            lemma : record { def =  λ x → x o< sup-o ( λ x → od→ord (ψ (X ∩ (ord→od x )))) } ≡
+                    record { def =  λ x → x o< sup-o ( λ x → od→ord (ψ (ord→od x ))) } 
+            lemma = {!!} 
+         replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → x == ψ (repl-x {ψ} {X} {x} lt)
+         replacement→ {ψ} X x = {!!} 
          ∅-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}