diff HOD.agda @ 140:312e27aa3cb5

remove otrans again. start over
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 07 Jul 2019 23:02:47 +0900
parents 53077af367e9
children 21b2654985c4
line wrap: on
line diff
--- a/HOD.agda	Sun Jul 07 22:23:02 2019 +0900
+++ b/HOD.agda	Sun Jul 07 23:02:47 2019 +0900
@@ -16,7 +16,6 @@
 record HOD {n : Level}  : Set (suc n) where
   field
     def : (x : Ordinal {n} ) → Set n
-    otrans : {x : Ordinal {n} } → def x → { y : Ordinal {n} } → y o< x → def y
 
 open HOD
 open import Data.Unit
@@ -49,9 +48,7 @@
 
 -- Ordinal in HOD ( and ZFSet )
 Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n}
-Ord {n} a = record { def = λ y → y o< a ; otrans = lemma }  where
-   lemma : {x : Ordinal} → x o< a → {y : Ordinal} → y o< x → y o< a
-   lemma {x}  x<a {y} y<x = ordtrans {n} {y} {x} {a} y<x x<a
+Ord {n} a = record { def = λ y → y o< a }  
 
 od∅ : {n : Level} → HOD {n} 
 od∅ {n} = Ord o∅ 
@@ -94,9 +91,7 @@
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
 
 cseq : {n : Level} →  HOD {n} →  HOD {n}
-cseq x = record { def = λ y → def x (osuc y) ; otrans = lemma } where
-   lemma : {ox : Ordinal} → def x (osuc ox) → { oy : Ordinal}→ oy o< ox → def x (osuc oy)
-   lemma {ox}  oox<Ox {oy} oy<ox  = otrans x  oox<Ox (osucc oy<ox )
+cseq x = record { def = λ y → def x (osuc y) } where
 
 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
@@ -145,10 +140,6 @@
    ... | t with t (case2 (s< s<refl ) )
    c3 lx (OSuc .lx x₁) d not | t | ()
 
-transitive : {n : Level } { z y x : HOD {suc n} } → z ∋ y → y ∋ x → z  ∋ x
-transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {suc n} {x} {y} x∋y ) (  c<→o< {suc n} {y} {z} z∋y ) 
-... | t = otrans z z∋y (c<→o< {suc n} {x} {y} x∋y ) 
-
 ∅5 : {n : Level} →  { x : Ordinal {n} }  → ¬ ( x  ≡ o∅ {n} ) → o∅ {n} o< x
 ∅5 {n} {record { lv = Zero ; ord = (Φ .0) }} not = ⊥-elim (not refl) 
 ∅5 {n} {record { lv = Zero ; ord = (OSuc .0 ord) }} not = case2 Φ<
@@ -206,7 +197,7 @@
 o≡→¬c< : {n : Level} →  { x y : HOD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
 o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡  (orefl oeq ) (c<→o< lt) 
 
-∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ ; otrans = λ () } == od∅ {n} 
+∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ } == od∅ {n} 
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} (case1 ())
 eq← ∅0 {w} (case2 ())
@@ -236,9 +227,7 @@
 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
 
 ZFSubset : {n : Level} → (A x : HOD {suc n} ) → HOD {suc n}
-ZFSubset A x =  record { def = λ y → def A y ∧  def x y ; otrans = lemma }   where
-  lemma : {z : Ordinal} → def A z ∧ def x z → {y : Ordinal} → y o< z → def A y ∧ def x y
-  lemma {z} d {y} y<z = record { proj1 = otrans A (proj1 d) y<z ; proj2 = otrans x (proj2 d) y<z }
+ZFSubset A x =  record { def = λ y → def A y ∧  def x y }   where
 
 Def :  {n : Level} → (A :  HOD {suc n}) → HOD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
@@ -296,12 +285,7 @@
     ; isZF = isZF 
  } where
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → ((y : Ordinal {suc n} ) → X ∋ ord→od y  → ψ (ord→od y)) ∧ (X ∋ ord→od x )  ; otrans = lemma } where
-       lemma :  {x : Ordinal} → ((y : Ordinal) → X ∋ ord→od y → ψ (ord→od y)) ∧ (X ∋ ord→od x) →
-            {y : Ordinal} → y o< x → ((y₁ : Ordinal) → X ∋ ord→od y₁ → ψ (ord→od y₁)) ∧ (X ∋ ord→od y)
-       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)  )
+    Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) }
     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)  ))))
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
@@ -369,8 +353,7 @@
          ... | case1 eq = proj1 (def-subst (Ltx t∋x) (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl )  where
               Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
-         ... | case2 lt = otrans (Ord a) (proj1 (lemma1 lt) )
-                   (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where
+         ... | case2 lt = {!!} where
               sp =  sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
               minsup :  HOD
               minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
@@ -427,7 +410,7 @@
          union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
          union→ X z u xx | tri< a ¬b ¬c | ()
          union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b 
-         union→ X z u xx | tri> ¬a ¬b c = otrans X (proj1 xx) c
+         union→ X z u xx | tri> ¬a ¬b c = {!!}
          union← :  (X z : HOD) (X∋z : Union X ∋ z) → (X ∋  union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
          union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where
              lemma : X ∋ union-u {X} {z} X∋z
@@ -435,35 +418,12 @@
 
          -- ψ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 = 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 
-         -- ψ< = {!!}
+         selection : {ψ : HOD → Set (suc n)} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+         selection {X} {ψ} {y} = {!!}
          replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 = lemma 
-                ; proj2 = sup-o∋ψx
-             }
-            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← {ψ} X x lt = {!!}
          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
+         replacement→ {ψ} X x lt = contra-position lemma {!!} 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 ))
 
@@ -476,7 +436,7 @@
              lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁
              lemma1 {x₁} s = ⊥-elim  ( minimul-1 x not (ord→od x₁) lemma3 ) where
                  lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁))
-                 lemma3 = proj1 s x₁ (proj2 s)
+                 lemma3 = {!!}
              lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
              lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))