# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595120563 -32400
# Node ID 17adeeee0c2a651852f1ab413d0d7a93eadda2e9
# Parent  30de2d9b93c16fe0bf0e4cd611f57789f69c59b2
fix Select and Replace

diff -r 30de2d9b93c1 -r 17adeeee0c2a BAlgbra.agda
--- a/BAlgbra.agda	Sun Jul 19 03:24:39 2020 +0900
+++ b/BAlgbra.agda	Sun Jul 19 10:02:43 2020 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Ordinals
 module BAlgbra {n : Level } (O : Ordinals {n})   where
@@ -55,13 +56,13 @@
     lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
        (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x}))
 
-∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
+∩-Select : { A B : HOD } →  Select A (  λ x _ → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
 ∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
-    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) }
-    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
-    lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
-        record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
+    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
+    lemma1 {x} lt = record { proj1 = proj1 {!!} ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 {!!} )) }
+    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ _ → (A ∋ x₁) ∧ (B ∋ x₁))) x
+    lemma2 {x} lt = {!!} -- record { proj1 = proj1 lt ; proj2 =
+        -- record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
 
 dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
diff -r 30de2d9b93c1 -r 17adeeee0c2a LEMC.agda
--- a/LEMC.agda	Sun Jul 19 03:24:39 2020 +0900
+++ b/LEMC.agda	Sun Jul 19 10:02:43 2020 +0900
@@ -40,12 +40,12 @@
     ; _∋_ = _∋_ 
     ; _≈_ = _=h=_ 
     ; ∅  = od∅
-    ; Select = Select
+    ; Select = ?
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select 
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ ?
     isZFC = record {
        choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
        choice = λ A {X} A∋X not → is-in (choice-func X not)
diff -r 30de2d9b93c1 -r 17adeeee0c2a OD.agda
--- a/OD.agda	Sun Jul 19 03:24:39 2020 +0900
+++ b/OD.agda	Sun Jul 19 10:02:43 2020 +0900
@@ -260,8 +260,8 @@
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
-in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD 
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
+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 ) {!!} ))))  }
 
 _∩_ : ( A B : HOD ) → HOD 
 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
@@ -326,13 +326,13 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
-Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
-Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
-Replace : HOD  → (HOD  → 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 }
+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  {!!} }
+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 }
     ; 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) {!!} ))
         rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
         rmax< lt = proj1 lt
 Union : HOD  → HOD   
@@ -358,7 +358,7 @@
 OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) )   
 
 Power : HOD  → HOD 
-Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
+Power A = Replace (OPwr (Ord (od→ord A))) ( λ x _ → A ∩ x )
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
@@ -459,26 +459,27 @@
 
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
-selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-selection {ψ} {X} {y} = record {
-    proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
-  ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
+selection : {X y : HOD} → {ψ : (x : HOD ) → X ∋ x → Set n} → ((X ∋ y) → ψ y {!!} ) ⇔ (Select X ψ ∋ y)
+selection  {X} {y} {ψ} = record {
+    proj1 = λ cond → {!!} -- record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
+  ; proj2 = λ select → {!!} -- record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
   }
-sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ 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 )
-replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; 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→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
-replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
-    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
-            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)))
+
+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 )
+replacement← : (X x : HOD) →  {ψ : (y : HOD )→ X ∋ y  → HOD} → (X∋x : X ∋ x ) → Replace X ψ ∋ ψ x {!!}
+replacement←  X x {ψ} lt = record { proj1 =  sup-c<  {X} {x} ψ lt ; 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→ : (X x : HOD) {ψ : (y : HOD ) → X ∋ y → HOD}  → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y {!!} ))
+replacement→  X x {ψ} lt = contra-position lemma (lemma2 {!!} ) where
+    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y) {!!} )))
+            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y) {!!} ))
     lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
-        lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) =h= ψ (ord→od y))  
+        lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y) {!!} )) → (ord→od (od→ord x) =h= ψ (ord→od y) {!!})  
         lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
-    lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) )
-    lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso  ( proj2 not2 ))
+    lemma :  ( (y : HOD) → ¬ (x =h= ψ y {!!} )) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y) {!!} ) )
+    lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y) {!!} ) oiso  ( proj2 not2 ))
 
 ---
 --- Power Set
@@ -527,7 +528,7 @@
 power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
     a = od→ord A
     lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
-    lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t
+    lemma2 = replacement→  (OPwr (Ord (od→ord A))) t {λ x _ → A ∩ x} P∋t
     lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
     lemma3 y eq not = not (proj1 (eq→ eq t∋x))
     lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y)))
@@ -601,8 +602,8 @@
     lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
     lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
         lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
-    lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
-    lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
+    lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) {!!} ) (od→ord t)
+    lemma2 not = ⊥-elim ( not (od→ord t) {!!}  ) where
         lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
         lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A  )))
 
@@ -655,9 +656,9 @@
     ;   ε-induction = ε-induction 
     ;   infinity∅ = infinity∅
     ;   infinity = infinity
-    ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-    ;   replacement← = replacement←
-    ;   replacement→ = λ {ψ} → replacement→ {ψ}
+    ;   selection = λ {X}  {y} {ψ} → {!!} -- selection {X} {y} {ψ}
+    ;   replacement← = {!!} -- replacement←
+    ;   replacement→ = {!!} -- λ {ψ} → replacement→ {ψ}
     -- ;   choice-func = choice-func
     -- ;   choice = choice
     } 
diff -r 30de2d9b93c1 -r 17adeeee0c2a ODC.agda
--- a/ODC.agda	Sun Jul 19 03:24:39 2020 +0900
+++ b/ODC.agda	Sun Jul 19 10:02:43 2020 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Ordinals
 module ODC {n : Level } (O : Ordinals {n} ) where
@@ -87,12 +88,12 @@
     ; _∋_ = _∋_ 
     ; _≈_ = _=h=_ 
     ; ∅  = od∅
-    ; Select = Select
+    ; Select = {!!}
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select 
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ {!!}
     isZFC = record {
        choice-func = choice-func ;
        choice = choice
diff -r 30de2d9b93c1 -r 17adeeee0c2a OPair.agda
--- a/OPair.agda	Sun Jul 19 03:24:39 2020 +0900
+++ b/OPair.agda	Sun Jul 19 10:02:43 2020 +0900
@@ -156,7 +156,7 @@
     lemma | tri> ¬a ¬b c = {!!}
 
 _⊗_ : (A B : HOD) → HOD
-A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
+A ⊗ B  = Union ( Replace B (λ b _ → Replace A (λ a _ → < a , b > ) ))
 
 product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
 product→ {A} {B} {a} {b} A∋a B∋b = {!!}
diff -r 30de2d9b93c1 -r 17adeeee0c2a zf.agda
--- a/zf.agda	Sun Jul 19 03:24:39 2020 +0900
+++ b/zf.agda	Sun Jul 19 10:02:43 2020 +0900
@@ -16,8 +16,8 @@
      (_,_ : ( A B : ZFSet  ) → ZFSet)
      (Union : ( A : ZFSet  ) → ZFSet)
      (Power : ( A : ZFSet  ) → ZFSet)
-     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) 
-     (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
+     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → (X ∋ x) → Set m ) → ZFSet ) 
+     (Replace : (X : ZFSet) → ( (x : ZFSet ) → ( X ∋ x ) → ZFSet ) → ZFSet )
      (infinite : ZFSet)
        : Set (suc (n ⊔ suc m)) where
   field
@@ -33,7 +33,7 @@
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
   _⊆_ A B {x} = A ∋ x →  B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
+  A ∩ B = Select A (  λ x _ → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
   A ∪ B = Union (A , B)    
   ｛_｝ : ZFSet → ZFSet
@@ -55,10 +55,10 @@
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
-     selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
+     selection : ∀ { X y : ZFSet  } →  { ψ : (x : ZFSet ) → X ∋ x → Set m } → ( 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← : {ψ : 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← : ∀ ( 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  ) )
 
 record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where
   infixr  210 _,_
@@ -73,8 +73,8 @@
      _,_ : ( A B : ZFSet  ) → ZFSet
      Union : ( A : ZFSet  ) → ZFSet
      Power : ( A : ZFSet  ) → ZFSet
-     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet 
-     Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
+     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → ( X ∋ x ) → Set m ) → ZFSet 
+     Replace : (X : ZFSet ) → ( (x : ZFSet ) → ( X ∋ x ) → ZFSet ) → ZFSet
      infinite : ZFSet
      isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite