# HG changeset patch # User Shinji KONO # Date 1595899953 -32400 # Node ID d87492ae40401b53c4c783f833ce9c903ea3ace7 # Parent 59152f16125a6bd7270e67956629752a6c519f1d ... diff -r 59152f16125a -r d87492ae4040 OD.agda --- a/OD.agda Tue Jul 28 09:45:58 2020 +0900 +++ b/OD.agda Tue Jul 28 10:32:33 2020 +0900 @@ -389,6 +389,14 @@ -- ｛_｝ : ZFSet → ZFSet -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly +union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z +union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx + ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } )) +union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) +union← X z UX∋z = FExists _ lemma UX∋z where + lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) + lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } + data infinite-d : ( x : Ordinal ) → Set n where iφ : infinite-d o∅ isuc : {x : Ordinal } → infinite-d x → @@ -456,36 +464,6 @@ _=h=_ : (x y : HOD) → Set n x =h= y = od x == od y --- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) --- postulate f-extensionality : { n m : Level} → HE.Extensionality n m - -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) → - (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x - ind {x} prev lt = ind1 lt oiso where - ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x - ind1 {o∅} iφ refl = sym o∅≡od∅ - ind1 {_} (isuc {x₁} ltd) ox=x = begin - nat→ω (ω→nato (isuc ltd) ) - ≡⟨⟩ - Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd))) - ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩ - Union (ord→od x₁ , (ord→od x₁ , ord→od x₁)) - ≡⟨ trans ( sym oiso) ox=x ⟩ - x - ∎ where - open ≡-Reasoning - lemma0 : x ∋ ord→od x₁ - lemma0 = {!!} - lemma1 : infinite ∋ ord→od x₁ - lemma1 = {!!} - lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ - lemma with prev {ord→od x₁} lemma0 lemma1 - ... | t = {!!} - - - infixr 200 _∈_ -- infixr 230 _∩_ _∪_ @@ -497,6 +475,12 @@ pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x)) pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y)) +pair1 : { x y : HOD } → (x , y ) ∋ x +pair1 = case1 refl + +pair2 : { x y : HOD } → (x , y ) ∋ y +pair2 = case2 refl + empty : (x : HOD ) → ¬ (od∅ ∋ x) empty x = ¬x<0 @@ -510,13 +494,34 @@ ⊆→o< {x} {y} lt | tri> ¬a ¬b c with (incl lt) (o<-subst c (sym diso) refl ) ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) -union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z -union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx - ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } )) -union← : (X z : HOD) (X∋z : Union X ∋ z) → ¬ ( (u : HOD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) -union← X z UX∋z = FExists _ lemma UX∋z where - lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z)) - lemma {y} xx not = not (ord→od y) record { proj1 = d→∋ X (proj1 xx) ; proj2 = proj2 xx } +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- postulate f-extensionality : { n m : Level} → HE.Extensionality n m + +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) → + (lt : infinite ∋ x) → nat→ω (ω→nat x lt) ≡ x + ind {x} prev lt = ind1 lt oiso where + ind1 : {ox : Ordinal } → (ltd : infinite-d ox ) → ord→od ox ≡ x → nat→ω (ω→nato ltd) ≡ x + ind1 {o∅} iφ refl = sym o∅≡od∅ + ind1 (isuc {x₁} ltd) ox=x = begin + nat→ω (ω→nato (isuc ltd) ) + ≡⟨⟩ + Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd))) + ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩ + Union (ord→od x₁ , (ord→od x₁ , ord→od x₁)) + ≡⟨ trans ( sym oiso) ox=x ⟩ + x + ∎ where + open ≡-Reasoning + lemma0 : x ∋ ord→od x₁ + lemma0 = subst (λ k → odef k (od→ord (ord→od x₁))) (trans (sym oiso) ox=x) (λ not → not + (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 + lemma : nat→ω (ω→nato ltd) ≡ ord→od x₁ + lemma with prev {ord→od x₁} lemma0 lemma1 + ... | t = {!!} ψiso : {ψ : HOD → Set n} {x y : HOD } → ψ x → x ≡ y → ψ y ψiso {ψ} t refl = t