# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558186806 -32400
# Node ID a53ba59c5bdaeb50cea43e5c5a895e854b3c8e03
# Parent  0f3d98e975932854e5eb957dfe273cd71d4476c8
dom-ψ

diff -r 0f3d98e97593 -r a53ba59c5bda constructible-set.agda
--- a/constructible-set.agda	Sat May 18 16:28:10 2019 +0900
+++ b/constructible-set.agda	Sat May 18 22:40:06 2019 +0900
@@ -173,6 +173,7 @@
   field
     α : Ordinal {suc n}
     constructible : Ordinal {suc n} → Set n
+    -- constructible : (x : Ordinal {suc n} ) → x o< α → Set n
 
 open ConstructibleSet
 
@@ -187,10 +188,22 @@
     sup : S
     smax  : ∀ { x : S } → x ≤ X  → ψ x ≤ sup 
     suniq : {max : S} → ( ∀ { x :  S } → x ≤ X  → ψ x ≤ max ) → max ≤ sup 
-    repl : ( x : Ordinal {n} ) → Set n
 
 open SupR
 
+record dom-ψ {n m : Level} (X : ConstructibleSet {n}) (ψ : ConstructibleSet {n} → ConstructibleSet {n} ) :  Set (suc (suc n) ⊔ suc m) where
+  field
+    αψ : Ordinal {suc n}
+    inψ : (x : Ordinal {suc n} ) → Set m
+    X∋x : (x : ConstructibleSet {n} ) → inψ (α x) → X ∋ x
+    vψ : (x : Ordinal {suc n} ) → inψ x  → ConstructibleSet {n}
+    cset≡ψ : (x : ConstructibleSet {n} ) → (t : inψ (α x) ) → x ≡ ψ ( vψ (α x) t )
+
+open dom-ψ
+
+postulate 
+    ψ→C : {n m : Level} (X : ConstructibleSet {n})  (ψ : ConstructibleSet {n} → ConstructibleSet {n} ) → dom-ψ {n} {m} X ψ
+
 _⊆_ : {n : Level} → ( A B : ConstructibleSet  ) → ∀{ x : ConstructibleSet } →  Set (suc n)
 _⊆_ A B {x} = A ∋ x →  B ∋ x
 
@@ -201,7 +214,6 @@
 sup  (Sup {n} ψ X ) = suptraverse X (c∅ {n}) ψ 
 smax (Sup ψ X ) = {!!} 
 suniq (Sup ψ X ) = {!!}
-repl (Sup ψ X ) = {!!}
      
 open import Data.Unit
 open SupR
@@ -220,18 +232,13 @@
     ; infinite = {!!}
     ; isZF = {!!}
  } where
-    Select : (X : ConstructibleSet {n}) → (ConstructibleSet  {n} → Set (suc n)) → ConstructibleSet {n}
+    Select : (X : ConstructibleSet {n}) → (ConstructibleSet {n} → Set (suc n)) → ConstructibleSet {n}
     Select X ψ = record { α = α X ; constructible = λ x →  select x } where 
        select : Ordinal → Set n
        select x with  ψ (record { α = x ; constructible = λ x → constructible X x })
        ... | t = Lift n ⊤
     Replace : (X : ConstructibleSet {n} ) → (ConstructibleSet → ConstructibleSet) → ConstructibleSet
-    Replace X ψ  = record { α = α (sup supψ)  ; constructible = λ x → repl1 x }  where
-       supψ : SupR (λ x a → (α a ≡ α x) ∨ (a ∋ x)) ψ X
-       supψ = Sup ψ X
-       repl1 : Ordinal {suc n} → Set n
-       repl1 x with repl supψ x
-       ... | t = Lift n  ⊤
+    Replace X ψ  = record { α = αψ {n} {suc (suc n)} (ψ→C X ψ)  ; constructible = λ x → inψ (ψ→C X ψ) x }  
     _,_ : ConstructibleSet {n} → ConstructibleSet → ConstructibleSet
     a , b  = record { α = maxα (α a) (α b) ; constructible =  a∨b }  where
        a∨b : Ordinal {suc n} → Set n