# HG changeset patch # User Shinji KONO # Date 1685932407 -32400 # Node ID 9e26c9abfafb83754a1d2219fb3d179f0ac16cb5 # Parent 47d3cc596d682279f2f7a076019ebb215bde72bc fix PFOD diff -r 47d3cc596d68 -r 9e26c9abfafb src/ODUtil.agda --- a/src/ODUtil.agda Sun Jun 04 16:58:39 2023 +0900 +++ b/src/ODUtil.agda Mon Jun 05 11:33:27 2023 +0900 @@ -179,18 +179,24 @@ (* x , * x ) ∎ ) &iso uy ) ⟩ -- (* x , * x ) ∋ * y y ∎ ) x ¬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 )))) + ω-∈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≠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) ))) ) +ω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) → @@ -217,8 +223,8 @@ 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 (sym eq)) - ... | t = HE.cong₂ (λ j k → isuc {j} k ) (HE.≡-to-≅ (ω-prev-eq eq)) t + 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 @@ -234,12 +240,18 @@ ω→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) - ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym - (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq )))))) + (sym ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym + (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))) ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso +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) )) + 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 } → {Cb : HOD} → {rcb : RXCod B Cb ψb } diff -r 47d3cc596d68 -r 9e26c9abfafb src/PFOD.agda --- a/src/PFOD.agda Sun Jun 04 16:58:39 2023 +0900 +++ b/src/PFOD.agda Mon Jun 05 11:33:27 2023 +0900 @@ -56,7 +56,9 @@ data Hω2 : (i : Nat) ( x : Ordinal ) → Set n where hφ : Hω2 0 o∅ h0 : {i : Nat} {x : Ordinal } → Hω2 i x → - Hω2 (Suc i) (& (Union ((nat→ω i , nat→ω i) , * x ))) + Hω2 (Suc i) (& (Union (< nat→ω i , od∅ > , * x ))) + h1 : {i : Nat} {x : Ordinal } → Hω2 i x → + Hω2 (Suc i) (& (Union (< nat→ω i , nat→ω 1 > , * x ))) he : {i : Nat} {x : Ordinal } → Hω2 i x → Hω2 (Suc i) x @@ -67,33 +69,60 @@ open Hω2r -hw⊆POmega : {y : Ordinal} → Hω2r y → odef (Power Omega) y -hw⊆POmega {y} r = odmax1 (Hω2r.count r) (Hω2r.hω2 r) where - odmax1 : {y : Ordinal} (i : Nat) → Hω2 i y → odef (Power Omega) y +hw⊆POmega : {x : Ordinal} → Hω2r x → odef (Power (Power Omega )) x +hw⊆POmega {x} r = odmax1 (Hω2r.count r) (Hω2r.hω2 r) where + odmax1 : {y : Ordinal} (i : Nat) → Hω2 i y → odef (Power (Power Omega )) y odmax1 0 hφ z xz = ⊥-elim ( ¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz )) odmax1 (Suc i) (h0 {_} {y} hw) = pf01 where - pf00 : odef ( Power Omega) y + pf00 : odef ( Power (Power Omega)) y pf00 = odmax1 i hw - pf01 : odef (Power Omega) (& (Union ((nat→ω i , nat→ω i ) , * y))) + pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 0 > , * y))) pf01 z xz with subst (λ k → odef k z ) *iso xz ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where - pf02 : Omega-d z - pf02 with subst (λ k → odef k z) *iso ox + pf02 : (w : Ordinal) → odef (* z) w → Omega-d w + pf02 w zw with subst (λ k → odef k z) *iso ox + ... | case2 refl with subst (λ k → odef k w) *iso zw + ... | case1 refl = ω∋nat→ω {i} + ... | case2 refl = ω∋nat→ω {0} + pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw + ... | case1 refl = ω∋nat→ω {i} + ... | case2 refl = ω∋nat→ω {i} + ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where + pf03 : odef ( Power (Power Omega)) y + pf03 = odmax1 i hw + pf02 : (w : Ordinal) → odef (* z) w → Omega-d w + pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox) _ zw + odmax1 (Suc i) (h1 {_} {y} hw) = pf01 where + pf00 : odef ( Power (Power Omega)) y + pf00 = odmax1 i hw + pf01 : odef (Power (Power Omega)) (& (Union (< nat→ω i , nat→ω 1 > , * y))) + pf01 z xz with subst (λ k → odef k z ) *iso xz + ... | record { owner = owner ; ao = case1 refl ; ox = ox } = pf02 where + pf02 : (w : Ordinal) → odef (* z) w → Omega-d w + pf02 w zw with subst (λ k → odef k z) *iso ox + ... | case2 refl with subst (λ k → odef k w) *iso zw + ... | case1 refl = ω∋nat→ω {i} + ... | case2 refl = ω∋nat→ω {1} + pf02 w zw | case1 refl with subst (λ k → odef k w) *iso zw ... | case1 refl = ω∋nat→ω {i} ... | case2 refl = ω∋nat→ω {i} - ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf00 _ (subst (λ k → odef k z) *iso ox) + ... | record { owner = owner ; ao = case2 refl ; ox = ox } = pf02 where + pf03 : odef ( Power (Power Omega)) y + pf03 = odmax1 i hw + pf02 : (w : Ordinal) → odef (* z) w → Omega-d w + pf02 w zw = odmax1 i hw _ (subst (λ k → odef (* k) z) (&iso) ox) _ zw odmax1 (Suc i) (he {_} {y} hw) = pf00 where - pf00 : odef ( Power Omega) y + pf00 : odef ( Power (Power Omega)) y pf00 = odmax1 i hw -- -- Set of limited partial function of Omega -- HODω2 : HOD -HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power Omega) +HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = & (Power (Power Omega)) ; , * x )) ; i = Suc (HwStep.i pf01) ; isHw = h0 (HwStep.isHw pf01) } where pf01 : HwStep pf01 = list→hod t x = HwStep.x pf01 - list→hod (i1 ∷ t) = list→hod t + list→hod (just i1 ∷ t) = record { x = & (Union ( < nat→ω (HwStep.i pf01) , nat→ω 1 > , * x )) + ; i = Suc (HwStep.i pf01) ; isHw = h1 (HwStep.isHw pf01) } where + pf01 : HwStep + pf01 = list→hod t + x = HwStep.x pf01 + list→hod (nothing ∷ t) = list→hod t -Hω2→3 : (x : HOD) → HODω2 ∋ x → List Two +Hω2→3 : (x : HOD) → HODω2 ∋ x → List (Maybe Two) Hω2→3 x = lemma where - lemma : { y : Ordinal } → Hω2r y → List Two + lemma : { y : Ordinal } → Hω2r y → List (Maybe Two) lemma record { count = 0 ; hω2 = hφ } = [] - lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = i0 ∷ lemma record { count = i ; hω2 = hω3 } - lemma record { count = (Suc i) ; hω2 = (he hω3) } = i1 ∷ lemma record { count = i ; hω2 = hω3 } + lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } + lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i0 ∷ lemma record { count = i ; hω2 = hω3 } + lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 = hω3 } ω→2 : HOD ω→2 = Power Omega