# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1562505782 -32400
# Node ID 53077af367e90a024d30243b82eda6e2641cb9e1
# Parent  567084f2278f0ab4ab6da3a2538021454f92e527
dead end?

diff -r 567084f2278f -r 53077af367e9 HOD.agda
--- a/HOD.agda	Sun Jul 07 17:37:26 2019 +0900
+++ b/HOD.agda	Sun Jul 07 22:23:02 2019 +0900
@@ -302,21 +302,8 @@
        lemma {x} select {y} y<x = record { proj1 = proj1 select ; proj2 = y<X } where
            y<X : X ∋ ord→od y
            y<X = otrans X (proj2 select) (o<-subst y<x (sym diso) (sym diso)  )
-    in-codomain : {n : Level} → (X : HOD {suc n} ) → ( ψ : HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-    in-codomain {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (Ord y )))))
-            ; otrans = lemma } where
-          lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) →
-            {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁))))
-          lemma {x} notx {y} y<x noty = notx ( λ z prod → noty z ( record { proj1 = proj1 prod ; proj2 = {!!} } ))
-    Replace' : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-    Replace' X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧  ( x == ψ (Ord y)  ))))
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
-    Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ;
-         otrans = lemma } where
-       lemma :  {x : Ordinal} → (x o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) x →
-            {y : Ordinal} → y o< x → (y o< sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∧ def (in-codomain X ψ) y
-       lemma {x} repl {y} y<x = record { proj1 = ordtrans y<x (proj1 repl)
-         ; proj2 = otrans (in-codomain X ψ) (proj2 repl) y<x }
+    Replace X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧  ( x == ψ (Ord y)  ))))
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     Union : HOD {suc n} → HOD {suc n}
@@ -456,27 +443,29 @@
                                   ; 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)
+         replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
+         replacement← {ψ} X x lt = record { proj1 = lemma 
+                ; proj2 = sup-o∋ψx
              }
             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
+             sup-o∋ψx : Ord (sup-o (λ x₁ → od→ord (ψ (ord→od x₁)))) ∋ ord→od (od→ord (ψ x))
+             sup-o∋ψx = 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)
+             lemma  : (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 lt1 not = not (minα (od→ord x) (sup-x ( λ w → od→ord (ψ (ord→od w ))))) (record {
+                      proj1 = ?
+                    ; proj2 = subst₂ (λ k j → k == j ) refl oiso (o≡→== {!!}) } ) where
+                 lemma1 : y o< osuc ( od→ord (ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w ))) )))) 
+                 lemma1 = o<-subst (sup-lb lt1) diso refl
+                 lemma2 : ord→od y ≡ ψ (ord→od ( sup-x ( λ w → od→ord (ψ (ord→od w )))))
+                 lemma2 with osuc-≡< lemma1
+                 lemma2 | case1 refl = subst (λ k → ord→od y ≡ k ) oiso  refl
+                 lemma2 | case2 t = {!!}
+         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 {!!} (ord→== {!!} ) )
 
          ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq