diff HOD.agda @ 150:ebcbfd9d9c8e

fix some
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2019 22:37:10 +0900
parents 6e767ad3edc2
children b5a337fb7a6d
line wrap: on
line diff
--- a/HOD.agda	Mon Jul 08 19:45:59 2019 +0900
+++ b/HOD.agda	Mon Jul 08 22:37:10 2019 +0900
@@ -60,6 +60,7 @@
   c<→o<  : {n : Level} {x y : OD {n} }      → def y ( od→ord x ) → od→ord x o< od→ord y
   oiso   : {n : Level} {x : OD {n}}     → ord→od ( od→ord x ) ≡ x
   diso   : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
+  -- we should prove this in agda, but simply put here
   ==→o≡ : {n : Level} →  { x y : OD {suc n} } → (x == y) → x ≡ y
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal becomes a set
   -- o<→c<  : {n : Level} {x y : Ordinal {n} } → x o< y             → def (ord→od y) x 
@@ -74,8 +75,6 @@
   -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
   minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
-  -- we should prove this in agda, but simply put here
-  ===-≡ : {n : Level} { x y : OD {suc n}} → x == y  → x ≡ y
 
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
@@ -163,7 +162,18 @@
          t : (od→ord x) o< (od→ord a)
          t = c<→o< {suc n} {x} {a} lt 
 
--- o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
+o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
+o∅≡od∅ {n} = ==→o≡ lemma where
+     lemma0 :  {x : Ordinal} → def (ord→od o∅) x → def od∅ x
+     lemma0 {x} lt = o<-subst (c<→o< {suc n} {ord→od x} {ord→od o∅} (def-subst {suc n} {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
+     lemma1 :  {x : Ordinal} → def od∅ x → def (ord→od o∅) x
+     lemma1 (case1 ())
+     lemma1 (case2 ())
+     lemma : ord→od o∅ == od∅
+     lemma = record { eq→ = lemma0 ; eq← = lemma1 }
+
+ord-od∅ : {n : Level} → od→ord (od∅ {suc n}) ≡ o∅ {suc n}
+ord-od∅ {n} = sym ( subst (λ k → k ≡  od→ord (od∅ {suc n}) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )
 
 o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
@@ -207,7 +217,7 @@
 Def {n} A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )  
 
 OrdSubset : {n : Level} → (A x : Ordinal {suc n} ) → ZFSubset (Ord A) (Ord x) ≡ Ord ( minα A x )
-OrdSubset {n} A x = ===-≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+OrdSubset {n} A x = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
   lemma1 :  {y : Ordinal} → def (ZFSubset (Ord A) (Ord x)) y → def (Ord (minα A x)) y
   lemma1 {y} s with trio< A x
   lemma1 {y} s | tri< a ¬b ¬c = proj1 s
@@ -332,17 +342,16 @@
          replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
          replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
              lemma : def (in-codomain X ψ) (od→ord (ψ x))
-             lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k))
-                 {!!} } ))
+             lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
          replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma (lemma2 {!!}) where
-            lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (Ord y))))
-                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (Ord y)))
+         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+            lemma2 :  ¬ ((y : Ordinal) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
+                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)))
             lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
-                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (Ord y))) → (ord→od (od→ord x) == ψ (Ord y))  
+                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) == ψ (ord→od y))  
                 lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
-            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 ))
+            lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) )
+            lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso  ( proj2 not2 ))
 
          ---
          --- Power Set
@@ -407,7 +416,7 @@
                     ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
               lemma1 : {n : Level } {a : Ordinal {suc n}} { t : OD {suc n}}
                  → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
-              lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
+              lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
               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<   
 
@@ -435,7 +444,7 @@
               lemma3 : Def (Ord a) ∋ t
               lemma3 = ord-power← a t lemma0
               lemma4 : od→ord t ≡ od→ord (A ∩ Ord (od→ord t))
-              lemma4 = cong ( λ k → od→ord k ) ( ===-≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} ))
+              lemma4 = cong ( λ k → od→ord k ) ( ==→o≡ (subst (λ k → t == (A ∩ k)) {!!} {!!} ))
               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)} {od→ord t}
               ... | lt = o<-subst {suc n} {_} {_} {_} {_} lt (sym (subst (λ k → od→ord t ≡ k) lemma5 lemma4 )) refl where
@@ -480,7 +489,7 @@
          infinite : OD {suc n}
          infinite = Ord omega 
          infinity∅ : Ord omega  ∋ od∅ {suc n}
-         infinity∅ = o<-subst (case1 (s≤s z≤n) ) {!!} refl
+         infinity∅ = o<-subst (case1 (s≤s z≤n) ) (sym ord-od∅) refl
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
          infinity x lt = o<-subst ( lemma (od→ord x) lt ) eq refl where
               eq :  osuc (od→ord x) ≡ od→ord (Union (x , (x , x)))