# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595233336 -32400
# Node ID 853ead1b56b8fbee443567f727a78a9f6f24ff82
# Parent  d735beee689acb3ff4e5a556a644a15ac4496152
...

diff -r d735beee689a -r 853ead1b56b8 OD.agda
--- a/OD.agda	Mon Jul 20 17:08:16 2020 +0900
+++ b/OD.agda	Mon Jul 20 17:22:16 2020 +0900
@@ -340,9 +340,11 @@
 d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (ord→od x)
 d→∋ a lt = subst (λ k → odef a k ) (sym diso) lt
 
+--
+-- If we have LEM, Replace' is equivalent to Replace 
+--
 in-codomain' : (X : HOD  ) → ((x : HOD) → X ∋ x → HOD) → OD 
 in-codomain'  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ((lt : odef X y) →  x ≡ od→ord (ψ (ord→od y ) (d→∋ X lt) ))))  }
-
 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) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x }
       ; odmax = rmax ; <odmax = rmax< } where
@@ -497,22 +499,6 @@
     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 ))
 
-sup-c<' :  {X x : HOD} → (ψ : (x : 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←' : (X x : HOD) {ψ : (x : 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 = ? }))
-replacement→' :  (X x : HOD) → {ψ : (x : HOD) → X ∋ x → HOD} → (lt : Replace' X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y ? ))
-replacement→'  X x {ψ} lt = contra-position lemma (lemma2 (λ lt1 → ? )) 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} 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 ))
-
 ---
 --- Power Set
 ---
diff -r d735beee689a -r 853ead1b56b8 cardinal.agda
--- a/cardinal.agda	Mon Jul 20 17:08:16 2020 +0900
+++ b/cardinal.agda	Mon Jul 20 17:22:16 2020 +0900
@@ -64,7 +64,7 @@
    lemma : Ordinal → Ordinal → Ordinal
    lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
    lemma x y | p | no n  = o∅
-   lemma x y | p | yes f∋y = lemma2 ? where -- (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
+   lemma x y | p | yes f∋y = lemma2 {!!} where -- (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
            lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
            lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
            lemma2 (pair x1 y1) | yes p = y1