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

comparison OD.agda @ 311:bf01e924e62e

...

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Tue, 30 Jun 2020 11:08:22 +0900
parents	73a2a8ec9603
children	c1581ed5f38b

comparison

equal deleted inserted replaced

-:73a2a8ec9603
+:bf01e924e62e
 OPwr :  (A :  HOD ) → HOD
 OPwr  A = Ord ( sup-o A ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )
--- _⊆_ :  ( A B : HOD   ) → ∀{ x : HOD  } →  Set n
--- _⊆_ A B {x} = A ∋ x →  B ∋ x
 record _⊆_ ( A B : HOD   ) : Set (suc n) where
 field
 incl : { x : HOD } → A ∋ x →  B ∋ x
 open _⊆_
 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
 induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
--- minimal-2 : (x : HOD  ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
--- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} )
 HOD→ZF : ZF
 HOD→ZF   = record {
 ZFSet = HOD
 ; _∋_ = _∋_
 } where
 ZFSet = HOD             -- is less than Ords because of maxod
 Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD
 Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
 Replace : HOD  → (HOD  → HOD) → HOD
-Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋x → od→ord (ψ (ord→od x)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
+Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} } -- ( λ x → od→ord (ψ x))
 _∩_ : ( A B : ZFSet  ) → ZFSet
 A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }  ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
 Union : HOD  → HOD
 Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  } ; odmax = {!!} ; <odmax = {!!} }
 _∈_ : ( A B : ZFSet  ) → Set n
 selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
 selection {ψ} {X} {y} = record {
 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
 ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
 }
-sup-od : ( HOD → HOD ) →  HOD
+sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
-sup-od = {!!}
+sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
-sup-c< :  ( ψ : HOD  →  HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
-sup-c< = {!!}
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-replacement← {ψ} X x lt = record { proj1 =  {!!} ; proj2 = lemma } where -- sup-c< ψ {x}
+replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; proj2 = lemma } where
 lemma : odef (in-codomain X ψ) (od→ord (ψ x))
 lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
 replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
 lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
 proj1 = odef-subst  {_} {_} {(Ord a)} {z}
 ( t→A (odef-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
 lemma1 :  {a : Ordinal } { t : HOD }
 → (eq : ZFSubset (Ord a) t =h= t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
 lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
+lemma2 : def (od (Ord a)) (od→ord t)
+lemma2 = {!!}
 lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord a) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
-lemma = {!!} -- sup-o<
+lemma = sup-o< _ lemma2
 --
 -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
 -- then replace of all elements of the Power set by A ∩ y
 --
 lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 ))
 lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) →  ¬ ¬  (odef A (od→ord x))
 lemma5 {y} eq not = (lemma3 (ord→od y) eq) not
 power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-power← A t t→A = record { proj1 = {!!} ; proj2 = lemma2 } where
+power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where
 a = od→ord A
 lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
 lemma0 {x} t∋x = c<→o< (t→A t∋x)
 lemma3 : OPwr (Ord a) ∋ t
 lemma3 = ord-power← a t lemma0
 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
 A ∩ t
 ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
 t
 ∎
+lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
+lemma7 = {!!}
 lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
 lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
-lemma4 {!!} -- (sup-o<  {λ x → od→ord (A ∩ x)}  )
+lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
 lemma2 :  odef (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
 lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
 lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t))
 lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
 ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a))
 ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
 lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
 lemma lt y<x with osuc-≡< lt

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

comparison OD.agda @ 311:bf01e924e62e