diff HOD.agda @ 142:c30bc9f5bd0d

Power Set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2019 12:13:19 +0900
parents 21b2654985c4
children 21b9e78e9359
line wrap: on
line diff
--- a/HOD.agda	Mon Jul 08 00:20:30 2019 +0900
+++ b/HOD.agda	Mon Jul 08 12:13:19 2019 +0900
@@ -81,6 +81,9 @@
 Ord-ord : {n : Level } {ox : Ordinal {suc n}} → Ord ox ≡ ord→od ox
 Ord-ord {n} {px} = trans (sym oiso) (cong ( λ k → ord→od k ) (sym ord-Ord)) 
 
+Ord-ord-≡ : {n : Level } {t : OD {suc n}} → Ord (od→ord t) ≡ t
+Ord-ord-≡ {n} {t}  = subst₂ (λ k j → k ≡ j ) oiso oiso (cong (λ k → ord→od k) (sym ord-Ord))
+
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
@@ -122,6 +125,8 @@
 Ord==→≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
 Ord==→≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) c )
 
+otrans : {n : Level} {a x : Ordinal {n} } → def (Ord a) x → { y : Ordinal {n} } → y o< x → def (Ord a) y
+otrans {n} {a} {x} x<a {y} y<x = ordtrans y<x x<a
 
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
@@ -302,7 +307,7 @@
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
     _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
+    A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
     Power : OD {suc n} → OD {suc n}
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
@@ -351,12 +356,17 @@
          --
          POrd : {a : Ordinal } {t : OD} → Def (Ord a) ∋ t → Def (Ord a) ∋ Ord (od→ord t)
          POrd {a} {t} P∋t = o<→c< P∋t
+         ∩-≡ :  { a b : OD {suc n} } → ({x : OD {suc n} } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
+         ∩-≡ {a} {b} inc = record {
+            eq→ = λ {x} x<a → record { proj2 = x<a ;
+                 proj1 = def-subst {suc n} {_} {_} {b} {x} (inc (def-subst {suc n} {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
+            eq← = λ {x} x<a∩b → proj2 x<a∩b }
          ord-power→ : (a : Ordinal ) ( t : OD) → Def (Ord a) ∋ t → {x : OD} → 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 : OD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
               Ltx {n} {x} {t} lt = c<→o< lt
-         ... | case2 lt = {!!} where
+         ... | case2 lt = lemma3 where
               sp =  sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
               minsup :  OD
               minsup =  ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 
@@ -379,6 +389,8 @@
                     ≡⟨ sym eq1 ⟩
                       minsup

+              lemma3 : od→ord x o< a
+              lemma3 = otrans (proj1 (lemma1 lt) ) (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) )
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
          -- Power A is a sup of ZFSubset A t, so Power A ∋ t
@@ -397,15 +409,6 @@
               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<   
 
-         -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
-         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
-         power→ = {!!}
-         power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A = {!!} where 
-              a = od→ord A
-              ψ : OD → OD
-              ψ y = Def (Ord a) ∩ y
-
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
          union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
@@ -413,7 +416,8 @@
          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 = {!!}
+         union→ X z u xx | tri> ¬a ¬b c = {!!}     --- osuc ( od→ord z )) o<  od→ord u o< od→ord X
+
          union← :  (X z : OD) (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
@@ -441,6 +445,34 @@
             lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)) )
             lemma not y not2 = not (Ord y) (subst (λ k → k == ψ (Ord y)) oiso  ( proj2 not2 ))
 
+         -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y )
+         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x
+         power→ A t P∋t {x} t∋x = TransFiniteExists {suc n} {λ y → (t ==  (A ∩ ord→od y))}
+                 lemma4 lemma5  where
+              a = od→ord A
+              lemma2 : ¬ ( (y : OD) → ¬ (t ==  (A ∩ y)))
+              lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t
+              lemma3 : (y : OD) → t == ( A ∩ y ) → A ∋ x
+              lemma3 y eq = proj1 (eq→ eq t∋x)
+              lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y)))
+              lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 ))
+              lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) → def A (od→ord x)
+              lemma5 {y} eq = lemma3 (ord→od y) eq
+         power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+         power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 
+              a = od→ord A
+              lemma0 : {x : OD} → t ∋ x → Ord a ∋ x
+              lemma0 {x} t∋x = c<→o< (t→A t∋x)
+              lemma3 : Def (Ord a) ∋ t
+              lemma3 = ord-power← a t lemma0
+              lemma1 : od→ord t o< sup-o (λ x → od→ord (A ∩ ord→od x))
+              lemma1 with sup-o< {suc n} {λ x → od→ord (A ∩ ord→od x)} {{!!}}
+              ... | lt = {!!}
+              lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
+              lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma4 }) ) where
+                  lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
+                  lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) (sym Ord-ord-≡) (∩-≡ t→A ) ))
+
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
          ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq  
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
@@ -450,7 +482,8 @@
              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 = {!!}
+                 lemma3 = record { proj1 = def-subst {suc n} {_} {_} {minimul x not} {_} (proj1 s) refl (sym diso)
+                                 ; proj2 = proj2 (proj2 s) } 
              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) ))