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 )
 --