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

changeset 259:f714fe999102

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 05 Sep 2019 01:28:52 +0900
parents 63df67b6281c
children 8b85949bde00
files OD.agda
diffstat 1 files changed, 26 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Wed Sep 04 01:12:18 2019 +0900
+++ b/OD.agda	Thu Sep 05 01:28:52 2019 +0900
@@ -70,14 +70,13 @@
   c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
   oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
   diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  -- we should prove this in agda, but simply put here
   ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
   --   o<→c<  : {n : Level} {x y : Ordinal  } → x o< y → def (ord→od y) x 
   --   ord→od x ≡ Ord x results the same
   -- supermum as Replacement Axiom
-  sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal 
-  sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } →  ψ x  o<  sup-o ψ 
+  sup-o  :  Ordinal → ( Ordinal  → Ordinal ) →  Ordinal 
+  sup-o< :  {X : Ordinal} → { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → x o< X  →  ψ x  o<  sup-o X ψ 
   -- contra-position of mimimulity of supermum required in Power Set Axiom
   -- sup-x  : {n : Level } → ( Ordinal  → Ordinal ) →  Ordinal 
   -- sup-lb : {n : Level } → { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
@@ -107,14 +106,14 @@
 def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
 
-sup-od : ( OD  → OD ) →  OD 
-sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
+sup-od : OD → ( OD  → OD ) →  OD 
+sup-od X ψ = Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) )
 
-sup-c< : ( ψ : OD  →  OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x ))
-sup-c<  ψ {x} = def-subst  {_} {_} {Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
+sup-c< : {X : OD } ( ψ : OD  →  OD ) → ∀ {x : OD } → X ∋ x  → def ( sup-od X ψ ) (od→ord ( ψ x ))
+sup-c<  {X} ψ {x} lt = def-subst  {_} {_} {Ord ( sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
         lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
-    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
-    lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso)  )
+    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (od→ord X) (λ x → od→ord (ψ (ord→od x)))
+    lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< (c<→o< lt) ) refl (sym diso)  )
 
 otrans : {n : Level} {a x y : Ordinal  } → def (Ord a) x → def (Ord x) y → def (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
@@ -338,7 +337,7 @@
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  --   roughly x = A → Set 
 
 Def :  (A :  OD ) → OD 
-Def  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+Def  A = Ord ( sup-o (osuc (od→ord A)) ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
 
 
 _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
@@ -370,7 +369,7 @@
     Select : (X : OD  ) → ((x : OD  ) → Set n ) → OD 
     Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
     Replace : OD  → (OD  → OD  ) → OD 
-    Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+    Replace X ψ = record { def = λ x → (x o< sup-o (od→ord X) ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
     _∩_ : ( A B : ZFSet  ) → ZFSet
     A ∩ B = record { def = λ x → def A x ∧ def B x } 
     Union : OD  → OD   
@@ -450,7 +449,7 @@
             ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
            }
          replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
+         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} lt ; 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 oiso)} ))
          replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
@@ -493,8 +492,16 @@
               lemma1 :  {a : Ordinal } { t : OD }
                  → (eq : ZFSubset (Ord a) t == 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) (ord→od x)))
-              lemma = sup-o<   
+              lemma3 : {x : OD} → (lt : t ∋ x ) → Ord (od→ord t) ∋ x
+              lemma3 lt = c<→o< lt
+              lemma2 : ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → od→ord t o< osuc (od→ord (Ord a))
+              lemma2 t→A = lemma5 t→A where
+                  lemma6 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → {x : OD}  → Ord (od→ord t) ∋ x → Ord ( od→ord s)  ∋ x
+                  lemma6 = {!!}
+                  lemma5 : {t s : OD } → ({x : OD} → (t ∋ x → s ∋ x)) → od→ord t o< osuc ( od→ord s)
+                  lemma5 t→A = ⊆→o< ( λ z → lemma6 t→A )
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (osuc (od→ord (Ord a))) (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma = sup-o<  (lemma2 t→A)
 
          -- 
          -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
@@ -523,8 +530,6 @@
               lemma0 {x} t∋x = c<→o< (t→A t∋x)
               lemma3 : Def (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
-              lt1 : od→ord (A ∩ ord→od (od→ord t)) o< sup-o (λ x → od→ord (A ∩ ord→od x))
-              lt1 = sup-o<  {λ x → od→ord (A ∩ ord→od x)} {od→ord t}
               lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
               lemma4 = let open ≡-Reasoning in begin
                     A ∩ ord→od (od→ord t)
@@ -533,9 +538,11 @@
                  ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
                     t
                  ∎
-              lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
-              lemma1 = subst (λ k → od→ord k o< sup-o (λ x → od→ord (A ∩ ord→od x)))
-                  lemma4 (sup-o<  {λ x → od→ord (A ∩ ord→od x)} {od→ord t})
+              lemma5 : od→ord t o< od→ord (Def (Ord (od→ord A)))
+              lemma5 = {!!}
+              lemma1 : od→ord t o< sup-o (od→ord (Def (Ord (od→ord A)))) (λ x → od→ord (A ∩ ord→od x))
+              lemma1 = subst (λ k → od→ord k o< sup-o (od→ord (Def (Ord (od→ord A))))  (λ x → od→ord (A ∩ ord→od x)))
+                  lemma4 (sup-o< {od→ord (Def (Ord (od→ord A)))} {λ x → od→ord (A ∩ ord→od x)} {od→ord t} lemma5 )
               lemma2 :  def (in-codomain (Def (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))