Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 300:e70980bd80c7
-- the set of finite partial functions from ω to 2
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 23 Jun 2020 15:12:43 +0900 |
| parents | ef93c56ad311 |
| children | b012a915bbb5 |
line wrap: on
line diff
--- a/OD.agda Mon Jun 15 18:15:48 2020 +0900 +++ b/OD.agda Tue Jun 23 15:12:43 2020 +0900 @@ -208,8 +208,8 @@ ZFSubset : (A x : OD ) → OD 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 x) ) ) +OPwr : (A : OD ) → OD +OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A x) ) ) -- _⊆_ : ( A B : OD ) → ∀{ x : OD } → Set n -- _⊆_ A B {x} = A ∋ x → B ∋ x @@ -268,7 +268,7 @@ _∈_ : ( A B : ZFSet ) → Set n A ∈ B = B ∋ A Power : OD → OD - Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) + Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x ) -- ｛_｝ : ZFSet → ZFSet -- ｛ x ｝ = ( x , x ) -- it works but we don't use @@ -369,11 +369,11 @@ -- -- Transitive Set case -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t == t - -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t - -- Def A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) + -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t + -- OPwr A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) ) -- - ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t - ord-power← a t t→A = def-subst {_} {_} {Def (Ord a)} {od→ord t} + ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t + ord-power← a t t→A = def-subst {_} {_} {OPwr (Ord a)} {od→ord t} lemma refl (lemma1 lemma-eq )where lemma-eq : ZFSubset (Ord a) t == t eq→ lemma-eq {z} w = proj2 w @@ -387,10 +387,10 @@ lemma = sup-o< -- - -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first + -- Every set in OD 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 -- - -- Power A = Replace (Def (Ord (od→ord A))) ( λ y → A ∩ y ) + -- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y ) -- we have oly double negation form because of the replacement axiom -- @@ -398,7 +398,7 @@ power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where a = od→ord A lemma2 : ¬ ( (y : OD) → ¬ (t == (A ∩ y))) - lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t + lemma2 = replacement→ (OPwr (Ord (od→ord A))) t P∋t lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x) lemma3 y eq not = not (proj1 (eq→ eq t∋x)) lemma4 : ¬ ((y : Ordinal) → ¬ (t == (A ∩ ord→od y))) @@ -411,7 +411,7 @@ 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 : OPwr (Ord a) ∋ t lemma3 = ord-power← a t lemma0 lemma4 : (A ∩ ord→od (od→ord t)) ≡ t lemma4 = let open ≡-Reasoning in begin @@ -424,7 +424,7 @@ 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 : def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t) + lemma2 : def (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 == (A ∩ k)) (sym oiso) ( ∩-≡ t→A )))