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

changeset 405:85b328d3b96b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 28 Jul 2020 14:15:33 +0900
parents f7b844af9a50
children bf409d31184c
files OD.agda
diffstat 1 files changed, 13 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Tue Jul 28 13:34:25 2020 +0900
+++ b/OD.agda	Tue Jul 28 14:15:33 2020 +0900
@@ -497,6 +497,17 @@
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
 
+ω-prev-eq1 : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → ¬ (x o< y)
+ω-prev-eq1 {x} {y} eq not with eq→ (ord→== eq) {od→ord (ord→od y , ord→od y)} (λ not2 → not2 (od→ord (ord→od y , ord→od y))
+      record { proj1 = case2 refl ; proj2 = subst (λ k → odef k (od→ord (ord→od y))) {!!} (case1 refl) } )
+... | t = {!!}
+
+ω-prev-eq : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
+ω-prev-eq {x} {y} eq with trio< x y
+ω-prev-eq {x} {y} eq | tri< a ¬b ¬c = {!!}
+ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = b
+ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = {!!}
+
 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
 nat→ω-iso {i} = ε-induction1 {λ i →  (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i  } ind i where
      ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : infinite ∋ y) → nat→ω (ω→nat y lt) ≡ y) →
@@ -519,14 +530,12 @@
                   (od→ord (ord→od x₁ , ord→od x₁))  record {proj1 = pair2 ; proj2 = subst (λ k → odef k (od→ord (ord→od x₁))) (sym oiso) pair1 } )
                lemma1 : infinite ∋ ord→od x₁
                lemma1 = subst (λ k → odef infinite k) (sym diso) ltd
-               lemma5 : {x y : Ordinal} →  od→ord (Union (ord→od y , (ord→od y , ord→od y))) ≡ od→ord (Union (ord→od x , (ord→od x , ord→od x))) → x ≡ y
-               lemma5 {x} {y} eq = {!!}
                lemma3 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ltd ≅ ltd1
                lemma3 iφ iφ refl = HE.refl
                lemma3 iφ (isuc ltd1) eq = {!!}
                lemma3 (isuc ltd) iφ eq = {!!}
-               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (lemma5 (sym eq))
-               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (lemma5 eq)) t  
+               lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (sym eq))
+               ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅  (ω-prev-eq eq)) t  
                lemma2 : {x y : Ordinal} → (ltd : infinite-d x ) (ltd1 : infinite-d y ) → y ≡ x → ω→nato ltd ≡ ω→nato ltd1
                lemma2 {x} {y} ltd ltd1 eq = lemma6 eq (lemma3 {x} {y} ltd ltd1 eq)  where
                    lemma6 : {x y : Ordinal} → {ltd : infinite-d x } {ltd1 : infinite-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1