# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562488646 -32400
# Node ID 567084f2278f0ab4ab6da3a2538021454f92e527
# Parent  c7c9f3efc428e64eb7d051cc969dac004c546414
...

diff -r c7c9f3efc428 -r 567084f2278f HOD.agda
--- a/HOD.agda	Sun Jul 07 08:56:25 2019 +0900
+++ b/HOD.agda	Sun Jul 07 17:37:26 2019 +0900
@@ -446,19 +446,37 @@
              lemma : X ∋ union-u {X} {z} X∋z
              lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} X∋z refl ord-Ord
 
-         ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
-         ψiso {ψ} t refl = t
+         -- ψiso :  {ψ : HOD {suc n} → Set (suc n)} {x y : HOD {suc n}} → ψ x → x ≡ y   → ψ y
+         -- ψiso {ψ} t refl = t
          selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
          selection {X} {ψ} {y} =  record { proj1 = λ s → record {
              proj1 = λ y1 y1<X → proj1 s (ord→od y1) y1<X ; proj2 = subst (λ k → def X k ) (sym diso) (proj2 s) }
-           ; proj2 = λ s → record { proj1 = λ y1 dy1 → subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
+           ; proj2 = λ s → record { proj1 = λ y1 dy1 →
+                  subst (λ k → ψ k ) oiso ((proj1 s) (od→ord y1) (def-subst {suc n} {_} {_} {X} {_} dy1 refl (sym diso )))
                                   ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
+         -- ψ< :  {ψ : HOD {suc n} → HOD {suc n}} {x y y' : HOD {suc n}} →  ψ y ∋ x → ψ y' == x 
+         -- ψ< = {!!}
+         replacement←' : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace' X ψ ∋ ψ x
+         replacement←' {ψ} X x lt = record { proj1 = {!!}
+                ; proj2 =  def-subst {suc n} {_} {_} {Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁))))}
+                    { od→ord (ord→od (od→ord (ψ x)))} (sup-c< ψ {x}) refl (sym diso)
+             }
+            where
+             --  (y : Ordinal) → Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od y →
+             --          ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁)))
+             lemma : (y : Ordinal) → ((y₁ : Ordinal) → ¬ def X y₁ ∧ (ord→od y == ψ (Ord y₁))) → {!!}
+             lemma y not = {!!}
+         replacement→' : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace' X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y))
+         replacement→' {ψ} X x lt = contra-position lemma (proj1 lt (od→ord x) (proj2 lt)) where
+            lemma :  ( (y : HOD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
+            lemma not y not2 = not (ord→od y) (subst₂ ( λ k j → k == j ) oiso (cong (λ k → ψ k ) Ord-ord ) (proj2 not2 ))
+                -- ord→od (od→ord x) == ψ (Ord y)
          replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
          replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; 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 (trans Ord-ord oiso ))} ))
-         replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (ψ x == y))
-         replacement→ {ψ} X x lt not = ⊥-elim ( not (ψ x) (ord→== refl ) )
+         replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x == ψ y))
+         replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!} ) )
 
          ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
diff -r c7c9f3efc428 -r 567084f2278f ordinal-definable.agda
--- a/ordinal-definable.agda	Sun Jul 07 08:56:25 2019 +0900
+++ b/ordinal-definable.agda	Sun Jul 07 17:37:26 2019 +0900
@@ -419,8 +419,8 @@
          replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; 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→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (ψ x == y))
-         replacement→ {ψ} X x lt not = ⊥-elim ( not (ψ x) (ord→== refl ) )
+         replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
+         replacement→ {ψ} X x lt not = ⊥-elim ( not {!!} (ord→== {!!} ) )
          ∅-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} 
diff -r c7c9f3efc428 -r 567084f2278f zf.agda
--- a/zf.agda	Sun Jul 07 08:56:25 2019 +0900
+++ b/zf.agda	Sun Jul 07 17:37:26 2019 +0900
@@ -22,8 +22,8 @@
 open import Relation.Nullary
 open import Relation.Binary
 
-contra-position : {n : Level } {A B : Set n} → (A → B) → ¬ B → ¬ A 
-contra-position {n} {A} {B}  f ¬b a = ¬b ( f a ) 
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a ) 
 
 infixr  130 _∧_
 infixr  140 _∨_
@@ -78,7 +78,7 @@
      selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  Set m } → ∀ {  y : ZFSet  } →  (((y : ZFSet) → 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→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
    -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
    -- axiom-of-choice : Set (suc n) 
    -- axiom-of-choice = ?