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

changeset 158:b97b4ee06f01

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Union trans finite
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 14 Jul 2019 17:26:57 +0900
parents afc030b7c8d0
children 3675bd617ac8
files HOD.agda ordinal.agda
diffstat 2 files changed, 19 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/HOD.agda	Sun Jul 14 08:04:16 2019 +0900
+++ b/HOD.agda	Sun Jul 14 17:26:57 2019 +0900
@@ -326,15 +326,20 @@
          Union-o : (X : Ordinal {suc n}) → OD {suc n}
          Union-o X = record { def = λ y → osuc y o< X }
 
---         union-ou : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
---         union-ou {X} {z} U>z = ord→od  ( osuc ( od→ord z ) )
---         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union-o x ∋ z
---         ord-union→ x z u plt = {!!}
---         ord-union← :  (x : Ordinal) (z : OD) (UX∋z : Union-o x ∋ z)
---                 → (Ord x ∋  union-ou {Ord x} {z} {!!} ) ∧ (union-ou {Ord x} {z} {!!} ∋ z )
---         ord-union← x z UX∋z = record { proj1 = lemma ; proj2 = {!!} } where
---             lemma : Ord x ∋ union-ou {Ord x} {z} {!!}
---             lemma = def-subst {suc n} {_} {_} {Ord x} {_} UX∋z refl (sym diso)
+         union-ou : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
+         union-ou {X} {z} U>z = ord→od  ( osuc ( od→ord z ) )
+         ord-union→ :  (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union-o x ∋ z
+         ord-union→ x z u plt with trio< ( od→ord u ) ( osuc ( od→ord z ))
+         ord-union→ X z u xx | tri< a ¬b ¬c with  osuc-< a (c<→o< (proj2 xx))
+         ord-union→ X z u xx | tri< a ¬b ¬c | ()
+         ord-union→ X z u xx | tri≈ ¬a b ¬c = def-subst (c<→o< (proj1 xx )) refl refl where
+         ord-union→ X z u xx | tri> ¬a ¬b c = {!!}
+
+         ord-union← :  (x : Ordinal) (z : OD) (UX∋z : Union-o x ∋ z)
+                 → (Ord x ∋  union-ou {Ord x} {z} {!!} ) ∧ (union-ou {Ord x} {z} {!!} ∋ z )
+         ord-union← x z UX∋z = record { proj1 = lemma ; proj2 = {!!} } where
+             lemma : Ord x ∋ union-ou {Ord x} {z} {!!}
+             lemma = def-subst {suc n} {_} {_} {Ord x} {_} UX∋z refl (sym diso)
 
          union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
          union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) )
@@ -342,10 +347,9 @@
          union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
               ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
 
-         union-u' : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
-         union-u' {X} {z} U>z = record { def = λ x → ¬ ( (u : Ordinal ) → ¬ (def X u) ∧ (ord→od u ∋ z ) ∧ ( u ≡ x ) ) }
          union←' :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
-         union←' X z UX∋z =  TransFiniteExists {suc (suc n)} {λ x → {!!} } {!!} {!!} where
+         union←' X z UX∋z =  TransFiniteExists _ UX∋z
+             ( λ {y} xx not → not (ord→od y) (record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } ))
          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 UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where
              lemma : X ∋ union-u {X} {z} UX∋z
@@ -428,7 +432,7 @@
          -- 
          -- 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))}
+         power→ A t P∋t {x} t∋x = TransFiniteExists _ -- (λ y → (t ==  (A ∩ ord→od y)))
                  lemma4 lemma5  where
               a = od→ord A
               lemma2 : ¬ ( (y : OD) → ¬ (t ==  (A ∩ y)))
--- a/ordinal.agda	Sun Jul 14 08:04:16 2019 +0900
+++ b/ordinal.agda	Sun Jul 14 17:26:57 2019 +0900
@@ -324,9 +324,9 @@
 --  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
 --      may be we can prove this...
 postulate 
- TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } 
+ TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
-  → {p : Set n} ( P : { y : Ordinal {n} } →  ψ y → p )
+  → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
   → p
 
 -- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where