diff HOD.agda @ 138:567084f2278f

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2019 17:37:26 +0900
parents c7c9f3efc428
children 53077af367e9
line wrap: on
line diff
--- 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