Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 127:870fe02c7a07
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Jul 2019 16:03:15 +0900 |
| parents | 1114081eb51f |
| children | 69a845b82854 |
| files | HOD.agda ordinal.agda |
| diffstat | 2 files changed, 28 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Mon Jul 01 01:27:25 2019 +0900 +++ b/HOD.agda Mon Jul 01 16:03:15 2019 +0900 @@ -345,28 +345,35 @@ -- then ZFSubset A ≡ t or ZFSubset A ∋ t. In the former case ZFSubset A ∋ x implies A ∋ x -- In case of later, ZFSubset A ∋ t and t ∋ x implies ZFSubset A ∋ x by transitivity -- + POrd : {A t : HOD} → Power A ∋ t → Power A ∋ Ord (od→ord t) + POrd {A} {t} P∋t = o<→c< P∋t power→ : (A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x - power→ A t P∋t {x} t∋x with osuc-≡< (sup-lb P∋t) - ... | case1 eq = proj1 (def-subst t∋x (sym (subst₂ (λ j k → j ≡ k ) oiso oiso ( cong (λ k → ord→od k) (sym eq) ))) refl ) - ... | case2 lt = otrans A (proj1 (lemma lt )) (c<→o< {suc n} {x} {t} t∋x) where + 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 : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x + Ltx {n} {x} {t} lt = c<→o< lt + ... | case2 lt = otrans A (proj1 (lemma1 lt) ) + (c<→o< {suc n} {x} {Ord (od→ord t)} (Ltx t∋x) ) where minsup : HOD minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) - lemma : od→ord t o< od→ord minsup → minsup ∋ t - lemma lt = {!!} + Ltx : {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x + Ltx {n} {x} {t} lt = c<→o< lt + lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t) + lemma1 lt = ? -- -- 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 -- power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t power← A t t→A = def-subst {suc n} {_} {_} {Power A} {od→ord t} - lemma refl lemma1 where + lemma refl (lemma1 lemma-eq )where lemma-eq : ZFSubset A t == t eq→ lemma-eq {z} w = proj2 w eq← lemma-eq {z} w = record { proj2 = w ; proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } - lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t - lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ lemma-eq )) + lemma1 : {n : Level } { A t : HOD {suc n}} → (eq : ZFSubset A t == t) → od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t + lemma1 {n} {A} {t} eq = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq )) lemma : od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x))) lemma = sup-o< union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
--- a/ordinal.agda Mon Jul 01 01:27:25 2019 +0900 +++ b/ordinal.agda Mon Jul 01 16:03:15 2019 +0900 @@ -170,6 +170,12 @@ maxαd x y | tri≈ ¬a b ¬c = x maxαd x y | tri> ¬a ¬b c = x +minαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx +minαd x y with triOrdd x y +minαd x y | tri< a ¬b ¬c = x +minαd x y | tri≈ ¬a b ¬c = y +minαd x y | tri> ¬a ¬b c = x + _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n) a o≤ b = (a ≡ b) ∨ ( a o< b ) @@ -212,10 +218,15 @@ maxα : {n : Level} → Ordinal {n} → Ordinal → Ordinal maxα x y with <-cmp (lv x) (lv y) -maxα x y | tri< a ¬b ¬c = x -maxα x y | tri> ¬a ¬b c = y +maxα x y | tri< a ¬b ¬c = y +maxα x y | tri> ¬a ¬b c = x maxα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = maxαd (ord x) (ord y) } +minα : {n : Level} → Ordinal {n} → Ordinal → Ordinal +minα x y with <-cmp (lv x) (lv y) +minα x y | tri< a ¬b ¬c = x +minα x y | tri> ¬a ¬b c = y +minα x y | tri≈ ¬a refl ¬c = record { lv = lv x ; ord = minαd (ord x) (ord y) } -- -- max ( osuc x , osuc y ) --