# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595229764 -32400
# Node ID 8cade5f660bd1f2b32162de254483fc2dbab418f
# Parent  b265042be254b295760acd8006ffb04cc38bd69c
Select : (X : HOD  ) → ((x : HOD  ) → X ∋ x → Set n ) → HOD does not work

diff -r b265042be254 -r 8cade5f660bd OD.agda
--- a/OD.agda	Mon Jul 20 12:17:43 2020 +0900
+++ b/OD.agda	Mon Jul 20 16:22:44 2020 +0900
@@ -156,6 +156,9 @@
 _c<_ : ( x a : HOD  ) → Set n
 x c< a = a ∋ x 
 
+d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
+d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
+
 cseq :  HOD  →  HOD 
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
@@ -257,11 +260,11 @@
 odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
 odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
 
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
--- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- postulate f-extensionality : { n m : Level}  → Relation.Binary.PropositionalEquality.Extensionality n m
 
 in-codomain : (X : HOD  ) → ( ψ : (x : HOD ) → X ∋ x → HOD  ) → OD 
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( (y<X : odef X y ) →   ( x ≡ od→ord (ψ (ord→od y ) {!!} ))))  }
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( (y<X : odef X y ) →   ( x ≡ od→ord (ψ (ord→od y ) (d→∋ X y<X)))))  }
 
 _∩_ : ( A B : HOD ) → HOD 
 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
@@ -327,12 +330,14 @@
      ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
 Select : (X : HOD  ) → ((x : HOD  ) → X ∋ x → Set n ) → HOD 
-Select X ψ = record { od = record { def = λ x →  (x<X : odef X x ) →  ψ ( ord→od x ) {!!}  } ; odmax = odmax X ; <odmax = λ y → <odmax X  {!!} }
+Select X ψ = record { od = record { def = λ x →  odef X x ∧ ( (x<X : odef X x ) →  ψ ( ord→od x ) (d→∋ X x<X) ) } ; odmax = odmax X ;
+    <odmax = λ y → <odmax X (proj1 y) }
+
 Replace : (X : HOD  ) → ((x : HOD) → X ∋ x → HOD) → HOD 
-Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y) {!!} ))) ∧ def (in-codomain X ψ) x }
+Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y )))) ∧ def (in-codomain X ψ) x }
     ; odmax = rmax ; <odmax = rmax<} where 
         rmax : Ordinal
-        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) {!!} ))
+        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y) (d→∋ X X∋y ) ))
         rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
         rmax< lt = proj1 lt
 Union : HOD  → HOD   
@@ -457,13 +462,17 @@
     lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
     lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 
 
-ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
-ψiso {ψ} t refl = t
-selection : {X y : HOD} → {ψ : (x : HOD ) → X ∋ x → Set n} → ((X ∋ y) → ψ y {!!} ) ⇔ (Select X ψ ∋ y)
+ψiso : {X : HOD}  {ψ : (x : HOD ) → X ∋ x → Set n} {x y : HOD } → {lt : X ∋ x}{lt' : X ∋ y} → ψ x lt → x ≡ y → lt ≅ lt' → ψ y lt'
+ψiso {X} {ψ} t refl HE.refl = t
+
+selection : {X y : HOD} → {ψ : (x : HOD ) → X ∋ x → Set n} → ((X ∋ y) ∧ ((y∈X : X ∋ y) → ψ y y∈X)) ⇔ (Select X ψ ∋ y)
 selection  {X} {y} {ψ} = record {
-    proj1 = λ cond → {!!} -- record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
+    proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = λ x<X → ψiso {X} {ψ} (proj2 cond (proj1 cond)) (sym oiso) {!!}  }
   ; proj2 = λ select → {!!} -- record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
-  }
+  } where
+      lemma : {X x : HOD} ( x<X : X ∋ x) → x<X ≅ d→∋ X x<X
+      lemma {X} {x} x<X with (oiso {x} )
+      ... | t = {!!}
 
 sup-c< :  {X x : HOD} → (ψ : (y : HOD ) → X ∋ y → HOD) → (X∋x : X ∋ x ) → od→ord (ψ x X∋x ) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y) {!!} )))
 sup-c< {X} {x} ψ lt = subst (λ k → od→ord (ψ k {!!} ) o< _ ) oiso (sup-o< X lt )
@@ -656,7 +665,7 @@
     ;   ε-induction = ε-induction 
     ;   infinity∅ = infinity∅
     ;   infinity = infinity
-    ;   selection = λ {X}  {y} {ψ} → {!!} -- selection {X} {y} {ψ}
+    ;   selection = λ {X}  {y} {ψ} → selection {X} {y} {ψ}
     ;   replacement← = {!!} -- replacement←
     ;   replacement→ = {!!} -- λ {ψ} → replacement→ {ψ}
     -- ;   choice-func = choice-func
diff -r b265042be254 -r 8cade5f660bd filter.agda
--- a/filter.agda	Mon Jul 20 12:17:43 2020 +0900
+++ b/filter.agda	Mon Jul 20 16:22:44 2020 +0900
@@ -173,20 +173,6 @@
 
 open _f⊆_
 
-_f∩_ : (f g : PFunc) → PFunc
-f f∩ g = record { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
-              ; map = λ x p →  map f x (proj1 p) }
-
-_↑_ : (Nat → Two) → Nat → PFunc
-f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
-
-record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
-   field
-     gn  : Nat
-     f<n :  (f ↑ gn) f⊆ p
-
-open Gf
-
 record F-Filter {n : Level} (L : Set n) (PL : (L → Set n) → Set n) ( _⊆_ : L  → L → Set n)  (_∩_ : L → L → L ) : Set (suc n) where
    field
        filter : L → Set n
@@ -206,6 +192,20 @@
 -- m≤m⊔n  = Data.Nat._⊔_
 open import Data.Nat.Properties
 
+_f∩_ : (f g : PFunc) → PFunc
+f f∩ g = record { restrict = λ x → (restrict f x ) ∧ (restrict g x ) ∧ ((fr : restrict f x ) → (gr : restrict g x ) → map f x fr ≡ map g x gr)
+              ; map = λ x p →  map f x (proj1 p) }
+
+_↑_ : (Nat → Two) → Nat → PFunc
+f ↑ i = record { restrict = λ x → Lift n (x ≤ i) ; map = λ x _ → f x }
+
+record Gf (f : Nat → Two) (p : PFunc ) : Set (suc n) where
+   field
+     gn  : Nat
+     f<n :  (f ↑ gn) f⊆ p
+
+open Gf
+
 GF : (Nat → Two ) → F-Filter PFunc (λ x → Lift (suc n) One ) _f⊆_ _f∩_
 GF f = record {  
        filter = λ p → Gf f p
diff -r b265042be254 -r 8cade5f660bd zf.agda
--- a/zf.agda	Mon Jul 20 12:17:43 2020 +0900
+++ b/zf.agda	Mon Jul 20 16:22:44 2020 +0900
@@ -55,7 +55,7 @@
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
-     selection : ∀ { X y : ZFSet  } →  { ψ : (x : ZFSet ) → X ∋ x → Set m } → ( y∈X : y ∈ X ) →  ψ y y∈X  ⇔ (y ∈ Select X ψ ) 
+     selection : ∀ { X y : ZFSet  } →  { ψ : (x : ZFSet ) → X ∋ x → Set m } → (y ∈ X ∧ (( y∈X : 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← : ∀ ( X x : ZFSet  ) → (x∈X : x ∈ X ) → {ψ : (x : ZFSet ) → x ∈ X  → ZFSet} → ψ x x∈X ∈  Replace X ψ 
      replacement→ : ∀ ( X x : ZFSet  ) →  {ψ : (x : ZFSet ) → X ∋ x  → ZFSet} → ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  → (X∋y : X ∋ y ) →  ¬ ( x ≈ ψ y X∋y  ) )