Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1463:9c19a7177b8a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Jan 2024 11:05:21 +0900 |
| parents | 76df157f6a3f |
| children | 484f83b04b5d |
| files | src/OD.agda src/ODUtil.agda |
| diffstat | 2 files changed, 144 insertions(+), 125 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OD.agda Tue Jan 02 17:19:31 2024 +0900 +++ b/src/OD.agda Wed Jan 03 11:05:21 2024 +0900 @@ -464,34 +464,35 @@ lemma : o∅ ≡ & od∅ lemma = sym ord-od∅ +Omega-iso : {x : HOD } → od (Union (* (& x) , (* (& x) , * (& x)))) == od (Union (x , (x , x))) +Omega-iso {x} = record { eq→ = lemma2 ; eq← = lemma3 } where + lemma2 : {y : Ordinal} → Own (* (& x) , (* (& x) , * (& x))) y → Own (x , (x , x)) y + lemma2 {y} record { owner = owner ; ao = case1 ao ; ox = ox } = record { owner = owner ; ao = case1 lemma4 ; ox = ox } where + lemma4 : owner ≡ & x + lemma4 = trans ao ( ==→o≡ *iso ) + lemma2 {y} record { owner = owner ; ao = case2 ao ; ox = ox } = record { owner = owner ; ao = case2 lemma4 ; ox = ox } where + lemma4 : owner ≡ & (x , x) + lemma4 = trans ao ( ==→o≡ record { eq→ = lemma5 _ ; eq← = lemma6 _ } ) where + lemma5 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) + lemma5 y (case1 eq) = case1 (trans eq (sym (==→o≡ *iso== ) )) + lemma5 y (case2 eq) = case1 (trans eq (sym (==→o≡ *iso== ) )) + lemma6 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) + lemma6 y (case1 eq) = case1 (trans eq ((==→o≡ *iso== ) )) + lemma6 y (case2 eq) = case1 (trans eq ((==→o≡ *iso== ) )) + lemma3 : {y : Ordinal} → Own (x , (x , x)) y → Own (* (& x) , (* (& x) , * (& x))) y + lemma3 {y} record { owner = owner ; ao = (case1 ao) ; ox = ox } = record { owner = owner + ; ao = case1 (trans ao (==→o≡ *iso== )) ; ox = ox } + lemma3 {y} record { owner = owner ; ao = (case2 ao) ; ox = ox } = record { owner = owner + ; ao = case2 (trans ao (==→o≡ record { eq→ = lemma5 _ ; eq← = lemma4 _ })) ; ox = ox } where + lemma4 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) + lemma4 y (case1 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) )) + lemma4 y (case2 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) )) + lemma5 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) + lemma5 y (case1 eq) = case1 ( trans eq ((==→o≡ *iso== ) )) + lemma5 y (case2 eq) = case1 ( trans eq ((==→o≡ *iso== ) )) + infinity : (ho< : ODAxiom-ho<) → (x : HOD) → Omega ho< ∋ x → Omega ho< ∋ Union (x , (x , x )) -infinity ho< x lt = subst (λ k → odef (Omega ho<) k ) lemma (isuc {& x} lt) where - lemma : & (Union (* (& x) , (* (& x) , * (& x)))) ≡ & (Union (x , (x , x))) - lemma = ==→o≡ record { eq→ = lemma2 ; eq← = lemma3 } where - lemma2 : {y : Ordinal} → Own (* (& x) , (* (& x) , * (& x))) y → Own (x , (x , x)) y - lemma2 {y} record { owner = owner ; ao = case1 ao ; ox = ox } = record { owner = owner ; ao = case1 lemma4 ; ox = ox } where - lemma4 : owner ≡ & x - lemma4 = trans ao ( ==→o≡ *iso ) - lemma2 {y} record { owner = owner ; ao = case2 ao ; ox = ox } = record { owner = owner ; ao = case2 lemma4 ; ox = ox } where - lemma4 : owner ≡ & (x , x) - lemma4 = trans ao ( ==→o≡ record { eq→ = lemma5 _ ; eq← = lemma6 _ } ) where - lemma5 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) - lemma5 y (case1 eq) = case1 (trans eq (sym (==→o≡ *iso== ) )) - lemma5 y (case2 eq) = case1 (trans eq (sym (==→o≡ *iso== ) )) - lemma6 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) - lemma6 y (case1 eq) = case1 (trans eq ((==→o≡ *iso== ) )) - lemma6 y (case2 eq) = case1 (trans eq ((==→o≡ *iso== ) )) - lemma3 : {y : Ordinal} → Own (x , (x , x)) y → Own (* (& x) , (* (& x) , * (& x))) y - lemma3 {y} record { owner = owner ; ao = (case1 ao) ; ox = ox } = record { owner = owner - ; ao = case1 (trans ao (==→o≡ *iso== )) ; ox = ox } - lemma3 {y} record { owner = owner ; ao = (case2 ao) ; ox = ox } = record { owner = owner - ; ao = case2 (trans ao (==→o≡ record { eq→ = lemma5 _ ; eq← = lemma4 _ })) ; ox = ox } where - lemma4 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) - lemma4 y (case1 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) )) - lemma4 y (case2 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) )) - lemma5 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) - lemma5 y (case1 eq) = case1 ( trans eq ((==→o≡ *iso== ) )) - lemma5 y (case2 eq) = case1 ( trans eq ((==→o≡ *iso== ) )) +infinity ho< x lt = subst (λ k → odef (Omega ho<) k ) (==→o≡ Omega-iso) (isuc {& x} lt) pair→ : ( x y t : HOD ) → (x , y) ∋ t → ( t =h= x ) ∨ ( t =h= y ) pair→ x y t (case1 t≡x ) = case1 ( ord→== t≡x ) @@ -501,6 +502,15 @@ pair← x y t (case1 t=h=x) = case1 (==→o≡ t=h=x) pair← x y t (case2 t=h=y) = case2 (==→o≡ t=h=y) +pair-iso : {x y : HOD } → (* (& x) , * (& y)) =h= (x , y) +pair-iso {x} {y} = record { eq→ = lem01 ; eq← = lem00 } where + lem00 : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & y) → (z ≡ & (* (& x))) ∨ (z ≡ & (* (& y))) + lem00 {z} (case1 z=x) = case1 (trans z=x ((==→o≡ *iso== ) )) + lem00 {z} (case2 z=y) = case2 (trans z=y ((==→o≡ *iso== ) )) + lem01 : {z : Ordinal} → (z ≡ & (* (& x))) ∨ (z ≡ & (* (& y))) → (z ≡ & x) ∨ (z ≡ & y) + lem01 {z} (case1 z=x) = case1 (trans z=x (sym (==→o≡ *iso== ) )) + lem01 {z} (case2 z=y) = case2 (trans z=y (sym (==→o≡ *iso== ) )) + o<→c< : {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) o<→c< lt {z} ox = ordtrans ox lt
--- a/src/ODUtil.agda Tue Jan 02 17:19:31 2024 +0900 +++ b/src/ODUtil.agda Wed Jan 03 11:05:21 2024 +0900 @@ -1,33 +1,58 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} open import Level open import Ordinals -module ODUtil {n : Level } (O : Ordinals {n} ) where +import HODBase +import OD +module ODUtil {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) where open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Data.Nat.Properties open import Data.Empty +open import Data.Unit open import Relation.Nullary -open import Relation.Binary hiding ( _⇔_ ) +open import Relation.Binary hiding (_⇔_) +open import Relation.Binary.Core hiding (_⇔_) open import logic +import OrdUtil open import nat open Ordinals.Ordinals O open Ordinals.IsOrdinals isOrdinal -- open Ordinals.IsNext isNext -import OrdUtil open OrdUtil O -import OD -open OD O -open OD.OD -open ODAxiom odAxiom +-- Ordinal Definable Set + +open HODBase.HOD +open HODBase.OD + +open _∧_ +open _∨_ +open Bool + +open HODBase._==_ + +open HODBase.ODAxiom HODAxiom + +-- HOD = HODBase.HOD O +-- OD = HODBase.OD O +-- Ords = HODBase.Ords O +-- _==_ = HODBase._==_ O +-- ==-refl = HODBase.==-refl O +-- ==-trans = HODBase.==-trans O +-- ==-sym = HODBase.==-sym O +-- ⇔→== = HODBase.⇔→== O + +open OD O HODAxiom +-- open OD.OD +-- open ODAxiom odAxiom -- open ODAxiom-ho< odAxiom-ho< -open HOD -open _∧_ -open _==_ +-- open HOD +-- open _∧_ +-- open _==_ _⊂_ : ( A B : HOD) → Set n _⊂_ A B = ( & A o< & B) ∧ ( A ⊆ B ) @@ -46,8 +71,8 @@ lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x) lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) -∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A) -∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ } +∩-comm : { A B : HOD } → (A ∩ B) =h= (B ∩ A) +∩-comm {A} {B} = record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ } _∪_ : ( A B : HOD ) → HOD A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ; @@ -56,8 +81,8 @@ lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _) lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _) -x∪x≡x : { A : HOD } → (A ∪ A) ≡ A -x∪x≡x {A} = ==→o≡ record { eq← = λ {x} lt → case1 lt ; eq→ = lem00 } where +x∪x≡x : { A : HOD } → (A ∪ A) =h= A +x∪x≡x {A} = record { eq← = λ {x} lt → case1 lt ; eq→ = lem00 } where lem00 : {x : Ordinal} → odef A x ∨ odef A x → odef A x lem00 {x} (case1 ax) = ax lem00 {x} (case2 ax) = ax @@ -75,21 +100,6 @@ lemma {z} (case1 refl) = case1 refl lemma {z} (case2 refl) = case1 refl --- pair-<xy : {x y : HOD} → {n : Ordinal} → & x o< next n → & y o< next n → & (x , y) o< next n --- pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y) --- ... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho< --- ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho< --- ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho< - --- another form of Omega --- pair-ord< : {x : Ordinal } → Set n --- pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x) --- pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1 where --- lemmab0 : next (odmax (x , x)) ≡ next (& x) --- lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡) --- lemmab1 : & (x , x) o< next ( odmax (x , x)) --- lemmab1 = ho< - trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab) @@ -115,14 +125,6 @@ ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫ } ---postulate --- odaxion-ho< : ODAxiom-ho< --- ---open ODAxiom-ho< odaxion-ho< - --- ω<next-o∅ : {y : Ordinal} → Omega-d y → y o< next omega --- ω<next-o∅ {y} lt = <odmax Omega lt - nat→ω : Nat → HOD nat→ω Zero = od∅ nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) @@ -131,14 +133,19 @@ ω→nato iφ = Zero ω→nato (isuc lt) = Suc (ω→nato lt) -ω→nat : (n : HOD) → Omega ∋ n → Nat +ω→nat : (n : HOD) → Omega ho< ∋ n → Nat ω→nat n = ω→nato -ω∋nat→ω : {n : Nat} → def (od Omega) (& (nat→ω n)) -ω∋nat→ω {Zero} = subst (λ k → def (od Omega) k) (sym ord-od∅) iφ -ω∋nat→ω {Suc n} = subst (λ k → def (od Omega) k) lemma (isuc ( ω∋nat→ω {n})) where - lemma : & (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n))))) ≡ & (nat→ω (Suc n)) - lemma = subst (λ k → & (Union (k , ( k , k ))) ≡ & (nat→ω (Suc n))) (sym *iso) refl +ω→nat-cong : (n : HOD) → (x y : Omega ho< ∋ n) → ω→nat n x ≡ ω→nat n y +ω→nat-cong n x y = ? + +ω∋nat→ω : {n : Nat} → def (od (Omega ho<)) (& (nat→ω n)) +ω∋nat→ω {Zero} = subst (λ k → def (od (Omega ho<)) k) (sym ord-od∅) iφ +ω∋nat→ω {Suc n} = subst (λ k → Omega-d k) (sym (==→o≡ nat01)) nat00 where + nat00 : Omega-d (& (Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n)))))) + nat00 = isuc ( ω∋nat→ω {n}) + nat01 : Union (nat→ω n , ( nat→ω n , nat→ω n)) =h= Union (* (& (nat→ω n)) , (* (& (nat→ω n)) , * (& (nat→ω n)))) + nat01 = ==-sym Omega-iso pair1 : { x y : HOD } → (x , y ) ∋ x pair1 = case1 refl @@ -146,15 +153,15 @@ pair2 : { x y : HOD } → (x , y ) ∋ y pair2 = case2 refl -single : {x y : HOD } → (x , x ) ∋ y → x ≡ y -single (case1 eq) = ==→o≡ ( ord→== (sym eq) ) -single (case2 eq) = ==→o≡ ( ord→== (sym eq) ) +single : {x y : HOD } → (x , x ) ∋ y → x =h= y +single (case1 eq) = ord→== (sym eq) +single (case2 eq) = ord→== (sym eq) single& : {x y : Ordinal } → odef (* x , * x ) y → x ≡ y single& (case1 eq) = sym (trans eq &iso) single& (case2 eq) = sym (trans eq &iso) -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- postulate f-extensionality : { n m : Level} → HE.Extensionality n m pair=∨ : {a b c : Ordinal } → odef (* a , * b) c → ( a ≡ c ) ∨ ( b ≡ c ) @@ -163,7 +170,7 @@ ω-prev-eq1 : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y) ω-prev-eq1 {x} {y} eq x<y with eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl - ; ox = subst (λ k → odef k (& (* y))) (sym *iso) (case1 refl) } -- (* x , (* x , * x)) ∋ * y + ; ox = eq→ *iso== (case1 refl) } -- (* x , (* x , * x)) ∋ * y ... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u ... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin osuc y ≡⟨ sym (cong osuc &iso) ⟩ @@ -173,10 +180,7 @@ & (* x) ≡⟨ &iso ⟩ x ∎ ))) where open o≤-Reasoning O ... | case2 u=xx = ⊥-elim (o<¬≡ ( begin - x ≡⟨ single& (subst₂ (λ j k → odef j k ) (begin - * u ≡⟨ cong (*) u=xx ⟩ - * (& (* x , * x)) ≡⟨ *iso ⟩ - (* x , * x ) ∎ ) &iso uy ) ⟩ -- (* x , * x ) ∋ * y + x ≡⟨ single& ( eq← *iso== (subst₂ (λ j k → odef j k ) (cong (*) u=xx ) &iso uy)) ⟩ y ∎ ) x<y) where open ≡-Reasoning ω-prev-eq : {x y : Ordinal} → & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → y ≡ x @@ -185,11 +189,11 @@ ω-prev-eq {x} {y} eq | tri≈ ¬a b ¬c = (sym b) ω-prev-eq {x} {y} eq | tri> ¬a ¬b c = ⊥-elim (ω-prev-eq1 (sym eq) c) -ω-inject : {x y : HOD} → Union ( y , ( y , y)) ≡ Union ( x , ( x , x)) → y ≡ x -ω-inject {x} {y} eq = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( ω-prev-eq (cong (&) (subst₂ (λ j k → Union (j , (j , j)) ≡ Union (k , (k , k))) (sym *iso) (sym *iso) eq )))) +ω-inject : {x y : HOD} → Union ( y , ( y , y)) =h= Union ( x , ( x , x)) → y =h= x +ω-inject {x} {y} eq = ord→== ( ω-prev-eq (==→o≡ (==-trans Omega-iso (==-trans eq (==-sym Omega-iso))))) ω-∈s : (x : HOD) → Union ( x , (x , x)) ∋ x -ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = subst₂ (λ j k → odef j k ) (sym *iso) refl (case2 refl) } +ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl ; ox = eq→ *iso== (case2 refl) } ωs≠0 : (x : HOD) → ¬ ( Union ( x , (x , x)) ≡ od∅ ) ωs≠0 y eq = ⊥-elim ( ¬x<0 (subst (λ k → & y o< k ) ord-od∅ (c<→o< (subst (λ k → odef k (& y )) eq (ω-∈s y) ))) ) @@ -197,60 +201,65 @@ ωs0 : o∅ ≡ & (nat→ω 0) ωs0 = trans (sym ord-od∅) (cong (&) refl ) -nat→ω-iso : {i : HOD} → (lt : Omega ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i -nat→ω-iso {i} = ε-induction {λ i → (lt : Omega ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i } ind i where - ind : {x : HOD} → ({y : HOD} → x ∋ y → (lt : Omega ∋ y) → nat→ω (ω→nat y lt) ≡ y) → - (lt : Omega ∋ x) → nat→ω (ω→nat x lt) ≡ x - ind {x} prev lt = ind1 lt *iso where - ind1 : {ox : Ordinal } → (ltd : Omega-d ox ) → * 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 (* x₁ , (* x₁ , * x₁)) - ≡⟨ trans ( sym *iso) ox=x ⟩ - x - ∎ where - open ≡-Reasoning - lemma0 : x ∋ * x₁ - lemma0 = subst (λ k → odef k (& (* x₁))) (trans (sym *iso) ox=x) - record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = subst (λ k → odef k (& (* x₁))) (sym *iso) (case1 refl) } - lemma1 : Omega ∋ * x₁ - lemma1 = subst (λ k → odef Omega k) (sym &iso) ltd - lemma3 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-d y ) → y ≡ x → ltd ≅ ltd1 - lemma3 iφ iφ refl = HE.refl - lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) ))) - lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) ))) - lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (eq)) - ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq (sym eq))) t - lemma2 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-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 : Omega-d x } {ltd1 : Omega-d y } → y ≡ x → ltd ≅ ltd1 → ω→nato ltd ≡ ω→nato ltd1 - lemma6 refl HE.refl = refl - lemma : nat→ω (ω→nato ltd) ≡ * x₁ - lemma = trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → Omega-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 ) +nat→ω-iso : {i : HOD} → (lt : Omega ho< ∋ i ) → nat→ω ( ω→nat i lt ) =h= i +nat→ω-iso {i} lt = ? where + nat→ω-iso-ord : (x : Ordinal) → odef (Omega ho< ) x → nat→ω ( ω→nat (* x) ? ) =h= (* x) + nat→ω-iso-ord x OD.iφ = ? + nat→ω-iso-ord x (OD.isuc lt) = ? +-- -- ε-induction {λ i → Lift (suc n) ((lt : Omega ho< ∋ i ) → nat→ω ( ω→nat i lt ) =h= i) } ind i where +-- ind : {x : HOD} → ({y : HOD} → x ∋ y → Lift (suc n) ((lt : Omega ho< ∋ y) → nat→ω (ω→nat y lt) =h= y)) → +-- (Lift (suc n) ((lt : Omega ho< ∋ x) → nat→ω (ω→nat x lt) =h= x)) +-- ind {x} prev = ? where +-- ind1 : {ox : Ordinal } → (ltd : Omega-d ox ) → * ox =h= x → nat→ω (ω→nato ltd) =h= x +-- ind1 {o∅} iφ eq = ==-sym ? +-- ind1 (isuc {x₁} ltd) ox=x = ? where +-- -- begin +-- -- nat→ω (ω→nato (isuc ltd) ) +-- -- ≡⟨⟩ +-- -- Union (nat→ω (ω→nato ltd) , (nat→ω (ω→nato ltd) , nat→ω (ω→nato ltd))) +-- -- ≡⟨ cong (λ k → Union (k , (k , k ))) lemma ⟩ +-- -- Union (* x₁ , (* x₁ , * x₁)) +-- -- ≡⟨ trans ( sym ? ) ox=x ⟩ +-- -- x +-- -- ∎ where +-- open ≡-Reasoning +-- lemma0 : x ∋ * x₁ +-- lemma0 = eq→ ox=x (eq→ *iso== +-- record { owner = & ( * x₁ , * x₁ ) ; ao = case2 refl ; ox = eq→ *iso== (case1 refl) }) +-- lemma1 : Omega ho< ∋ * x₁ +-- lemma1 = subst (λ k → odef (Omega ho<) k) (sym &iso) ltd +-- lemma3 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-d y ) → y ≡ x → ? -- ltd ? ltd1 +-- lemma3 = ? +-- -- lemma3 iφ (isuc {y} ltd1) eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso eq (c<→o< (ω-∈s (* y)) ))) +-- -- lemma3 (isuc {y} ltd) iφ eq = ⊥-elim ( ¬x<0 (subst₂ (λ j k → j o< k ) &iso (sym eq) (c<→o< (ω-∈s (* y)) ))) +-- -- lemma3 (isuc {x} ltd) (isuc {y} ltd1) eq with lemma3 ltd ltd1 (ω-prev-eq (eq)) +-- -- ... | t = ? -- HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq (sym eq))) t +-- lemma2 : {x y : Ordinal} → (ltd : Omega-d x ) (ltd1 : Omega-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 : Omega-d x } {ltd1 : Omega-d y } → y ≡ x → ? → ω→nato ltd ≡ ω→nato ltd1 +-- lemma6 = ? -- refl HE.refl = refl +-- lemma : nat→ω (ω→nato ltd) =h= * x₁ +-- lemma = ? -- trans (cong (λ k → nat→ω k) (lemma2 {x₁} {_} ltd (subst (λ k → Omega-d k ) (sym &iso) ltd) &iso ) ) ( prev {* x₁} lemma0 lemma1 ) ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : Omega-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x ω→nat-iso0 Zero iφ eq = refl -ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) o∅≡od∅ )) -ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (subst (λ k → k ≡ od∅ ) *iso eq )) +ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) ? )) +ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (subst (λ k → k ≡ od∅ ) ? eq )) ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where lemma1 : * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i - lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k) + lemma1 eq = subst (λ k → * x ≡ k ) ? (cong (λ k → * k) (sym ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym - (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))) + (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym ? ) eq ))))))) ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i -ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso +ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) ? nat→ω-inject : {i j : Nat} → nat→ω i ≡ nat→ω j → i ≡ j nat→ω-inject {Zero} {Zero} eq = refl nat→ω-inject {Zero} {Suc j} eq = ⊥-elim ( ¬0=ux (trans (trans (sym ord-od∅) (cong (&) eq)) refl )) nat→ω-inject {Suc i} {Zero} eq = ⊥-elim ( ¬0=ux (trans (trans (sym ord-od∅) (cong (&) (sym eq))) refl )) -nat→ω-inject {Suc i} {Suc j} eq = cong Suc (nat→ω-inject {i} {j} ( ω-inject (eq) )) +nat→ω-inject {Suc i} {Suc j} eq = ? -- cong Suc (nat→ω-inject {i} {j} ( ω-inject ? )) Repl⊆ : {A B : HOD} (A⊆B : A ⊆ B) → { ψa : ( x : HOD) → A ∋ x → HOD } { ψb : ( x : HOD) → B ∋ x → HOD } → {Ca : HOD} → {rca : RXCod A Ca ψa } @@ -261,7 +270,7 @@ ; x=ψz = trans x=ψz (cong (&) (eq az) ) } PPP : {P : HOD} → Power P ∋ P -PPP {P} z pz = subst (λ k → odef k z ) *iso pz +PPP {P} z pz = eq← *iso== pz UPower⊆Q : {P Q : HOD} → P ⊆ Q → Union (Power P) ⊆ Q UPower⊆Q {P} {Q} P⊆Q {z} record { owner = y ; ao = ppy ; ox = yz } = P⊆Q (ppy _ yz) @@ -271,7 +280,7 @@ UPower∩ {P} each {p} {q} record { owner = x ; ao = ppx ; ox = xz } record { owner = y ; ao = ppy ; ox = yz } = record { owner = & P ; ao = PPP ; ox = lem03 } where lem03 : odef (* (& P)) (& (p ∩ q)) - lem03 = subst (λ k → odef k (& (p ∩ q))) (sym *iso) ( each (ppx _ xz) (ppy _ yz) ) + lem03 = eq→ *iso== ( each (ppx _ xz) (ppy _ yz) ) -- ∋-irr : {X x : HOD} → (a b : X ∋ x ) → a ≡ b -- ∋-irr {X} {x} _ _ = refl