# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562433572 -32400
# Node ID 3cc848664a86232d176ad21ecde038df7f77f926
# Parent  b60b6e8a57b0b4eebea68b9d1cd30a505448eef8
... should use Select in Replace

diff -r b60b6e8a57b0 -r 3cc848664a86 HOD.agda
--- a/HOD.agda	Sun Jul 07 00:51:12 2019 +0900
+++ b/HOD.agda	Sun Jul 07 02:19:32 2019 +0900
@@ -233,13 +233,6 @@
 csuc :  {n : Level} →  HOD {suc n} → HOD {suc n}
 csuc x = Ord ( osuc ( od→ord x ))
 
-in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))
-    ; otrans = lemma } where
-  lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) →
-    {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁))))
-  lemma {x} notx {y} y<x noty = {!!}
-
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
@@ -302,6 +295,19 @@
     ; infinite = Ord omega
     ; isZF = isZF 
  } where
+    Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
+    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
+       lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
+            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
+       lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
+           y<X : X ∋ ord→od y
+           y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso)  )
+    in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n}
+    in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))
+            ; otrans = lemma } where
+          lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) →
+            {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁))))
+          lemma {x} notx {y} y<x noty = notx ( λ z prod → noty z ( record { proj1 = proj1 prod ; proj2 = {!!} } ))
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
     Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ;
          otrans = lemma } where
@@ -309,13 +315,6 @@
             {y : Ordinal} → y o< x → (y o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) y
        lemma {x} repl {y} y<x = record { proj1 = ordtrans y<x (proj1 repl)
          ; proj2 = otrans (in-codomain X ψ) (proj2 repl) y<x }
-    Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
-       lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
-            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
-       lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
-           y<X : X ∋ ord→od y
-           y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso)  )
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     Union : HOD {suc n} → HOD {suc n}