Members/kono/Proof/ZF-in-agda: HOD.agda comparison

comparison 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

comparison

equal deleted inserted replaced

-:53077af367e9
+:312e27aa3cb5
 -- Ordinal Definable Set
 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
 open Ordinal
 eq→ ( ⇔→== {n} {x} {y}  eq ) {z} m = proj1 eq m
 eq← ( ⇔→== {n} {x} {y}  eq ) {z} m = proj2 eq m
 -- 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
+Ord {n} a = record { def = λ y → y o< a }
-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
 od∅ : {n : Level} → HOD {n}
 od∅ {n} = Ord o∅
 postulate
 _c≤_ : {n : Level} →  HOD {n} →  HOD {n} → Set (suc n)
 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
+cseq x = record { def = λ y → def x (osuc y) } 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 )
 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
 o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y → Ord y ∋ Ord x
 c3 lx (Φ .lx) d not | t | ()
 c3 lx (OSuc .lx x₁) d not with not (  record { lv = lx ; ord = OSuc lx x₁ } )
 ... | 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 Φ<
 ∅5 {n} {record { lv = (Suc lv) ; ord = ord }} not = case1 (s≤s z≤n)
 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
 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 ())
 ∅< : {n : Level} →  { x y : HOD {n} } → def x (od→ord y ) → ¬ (  x  == od∅ {n} )
 csuc x = Ord ( osuc ( od→ord x ))
 -- 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
+ZFSubset A x =  record { def = λ y → def A y ∧  def x y }   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 }
 Def :  {n : Level} → (A :  HOD {suc n}) → HOD {suc n}
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
 OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
 ; Replace = Replace
 ; infinite = Ord omega
 ; 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
+Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( ord→od x )) }
-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)  )
 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}
 x , y = Ord (omax (od→ord x) (od→ord y))
 Union : HOD {suc n} → HOD {suc n}
 ord-power→ : (a : Ordinal ) ( t : HOD) → Def (Ord a) ∋ t → {x : HOD} → t ∋ x → Ord a ∋ x
 ord-power→ a t P∋t {x} t∋x with osuc-≡<  (sup-lb  (POrd P∋t))
 ... | 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) )
+... | case2 lt = {!!} where
-(c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) 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)))))
 Ltx :   {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
 Ltx {n} {x} {t} lt = c<→o< lt
 union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
 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
 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
-selection : {X : HOD } {ψ : (x : HOD ) → Set (suc n)} {y : HOD} → (((y₁ : HOD) → X ∋ y₁ → ψ y₁) ∧ (X ∋ y)) ⇔ (Select X ψ ∋ y)
+selection : {ψ : HOD → Set (suc n)} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-selection {X} {ψ} {y} =  record { proj1 = λ s → record {
+selection {X} {ψ} {y} = {!!}
-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
--- ψ< = {!!}
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-replacement← {ψ} X x lt = record { proj1 = lemma
+replacement← {ψ} X x lt = {!!}
-; 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→ : {ψ : 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 ))
 ∅-iso :  {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
 proj1 (regularity x not ) = x∋minimul x not
 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where
 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) ))
 extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d

Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison HOD.agda @ 140:312e27aa3cb5