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

changeset 306:b07fc3ef5aab

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix sup
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 29 Jun 2020 20:33:19 +0900
parents 4804f3f3485f
children d5c5d87b72df
files OD.agda
diffstat 1 files changed, 14 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Mon Jun 29 18:37:31 2020 +0900
+++ b/OD.agda	Mon Jun 29 20:33:19 2020 +0900
@@ -100,11 +100,8 @@
   diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
   ==→o≡ : { x y : HOD  } → (od x == od y) → x ≡ y
   -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
-  sup-od : ( HOD  → HOD ) →  HOD 
-  sup-c< :  ( ψ : HOD  →  HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
-  -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use
-  -- sup-x  : {n : Level } → ( OD → Ordinal ) →  Ordinal 
-  -- sup-lb : {n : Level } → { ψ : OD →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
+  sup-o  :  (A : HOD) → (( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
+  sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
 
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
@@ -125,10 +122,10 @@
 od∅ : HOD  
 od∅  = Ord o∅ 
 
-sup-o  :  ( HOD → Ordinal ) →  Ordinal 
-sup-o  = {!!}
-sup-o< :  { ψ : HOD →  Ordinal } → ∀ {x : HOD } → ψ x  o<  sup-o ψ 
-sup-o< = {!!}
+sup-od : ( HOD → HOD ) →  HOD 
+sup-od = {!!}
+sup-c< :  ( ψ : HOD  →  HOD ) → ∀ {x : HOD } → def (od ( sup-od ψ )) (od→ord ( ψ x ))
+sup-c< = {!!}
 
 odef : HOD → Ordinal → Set n
 odef A x = def ( od A ) x
@@ -147,7 +144,7 @@
 x c< a = a ∋ x 
 
 cseq : {n : Level} →  HOD  →  HOD 
-cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = ? } where
+cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = {!!} } where
 
 odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
 odef-subst df refl refl = df
@@ -229,7 +226,7 @@
 ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = {!!} ; <odmax = {!!} }  --   roughly x = A → Set 
 
 OPwr :  (A :  HOD ) → HOD 
-OPwr  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A x) ) )   
+OPwr  A = Ord ( sup-o {!!} {!!} ) --  ( λ x → od→ord ( ZFSubset A x) ) )   
 
 -- _⊆_ :  ( A B : HOD   ) → ∀{ x : HOD  } →  Set n
 -- _⊆_ A B {x} = A ∋ x →  B ∋ x
@@ -280,7 +277,7 @@
     Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
     Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = {!!} ; <odmax = {!!} }
     Replace : HOD  → (HOD  → HOD  ) → HOD 
-    Replace X ψ = record { od = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ x))) ∧ odef (in-codomain X ψ) x } ; odmax = {!!} ; <odmax = {!!} }
+    Replace X ψ = record { od = record { def = λ x → (x o< sup-o  {!!} {!!} ) ∧ 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 = {!!} ; <odmax = {!!} }
     Union : HOD  → HOD   
@@ -406,8 +403,8 @@
               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 ))
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o  (λ x → od→ord (ZFSubset (Ord a) x))
-              lemma = sup-o<  
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o {!!} {!!} --  (λ x → od→ord (ZFSubset (Ord a) x))
+              lemma = {!!} -- sup-o<  
 
          -- 
          -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
@@ -444,9 +441,9 @@
                  ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
                     t
                  ∎
-              lemma1 : od→ord t o< sup-o  (λ x → od→ord (A ∩ x))
-              lemma1 = subst (λ k → od→ord k o< sup-o   (λ x → od→ord (A ∩ x)))
-                  lemma4 (sup-o<  {λ x → od→ord (A ∩ x)}  )
+              lemma1 : od→ord t o< sup-o  {!!} {!!} -- (λ x → od→ord (A ∩ x))
+              lemma1 = subst (λ k → od→ord k o< sup-o  {!!} {!!}) --  (λ x → od→ord (A ∩ x)))
+                  lemma4 {!!} -- (sup-o<  {λ x → od→ord (A ∩ x)}  )
               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))