Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1472:d0b4be1cab0d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Jun 2024 19:23:56 +0900 |
| parents | e970149a6af5 |
| children | aca42b19db4c |
| files | src/ZProduct.agda src/bijection.agda src/cardinal.agda src/partfunc.agda |
| diffstat | 4 files changed, 324 insertions(+), 229 deletions(-) [+] |
line wrap: on
line diff
--- a/src/ZProduct.agda Sat Jun 22 12:39:58 2024 +0900 +++ b/src/ZProduct.agda Sat Jun 22 19:23:56 2024 +0900 @@ -424,10 +424,9 @@ record Injection (A B : Ordinal ) : Set n where field - i→ : (x : Ordinal ) → odef (* A) x → Ordinal - irr : (x : Ordinal ) → ( lt1 lt2 : odef (* A) x ) → i→ x lt1 ≡ i→ x lt2 - iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt ) - inject : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y + i→ : (x : Ordinal ) → Ordinal + iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x ) + inject : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ≡ i→ y → x ≡ y record HODBijection (A B : HOD ) : Set n where field
--- a/src/bijection.agda Sat Jun 22 12:39:58 2024 +0900 +++ b/src/bijection.agda Sat Jun 22 19:23:56 2024 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module bijection where @@ -47,8 +47,8 @@ bi-inject→ : {n m : Level} {R : Set n} {S : Set m} → (rs : Bijection R S) → {x y : R} → fun→ rs x ≡ fun→ rs y → x ≡ y bi-inject→ rs {x} {y} eq = subst₂ (λ j k → j ≡ k ) (fiso← rs _) (fiso← rs _) (cong (fun← rs) eq) -bi-∨ : {n m n1 m1 : Level } {A : Set n} {B : Set m} {C : Set n1} {D : Set m1} → (ab : Bijection A B) → (cd : Bijection C D ) - → Bijection (A ∨ C) (B ∨ D) +bi-∨ : {n m n1 m1 : Level } {A : Set n} {B : Set m} {C : Set n1} {D : Set m1} → (ab : Bijection A B) → (cd : Bijection C D ) + → Bijection (A ∨ C) (B ∨ D) bi-∨ {_} {_} {_} {_} {A} {B} {C} {D} ab cd = record { fun→ = fun→1 ; fun← = fun←1 @@ -64,7 +64,7 @@ fiso→1 : (x : B ∨ D) → fun→1 (fun←1 x) ≡ x fiso→1 (case1 a) = cong case1 (fiso→ ab a) fiso→1 (case2 c) = cong case2 (fiso→ cd c) - fiso←1 : (x : A ∨ C) → fun←1 (fun→1 x) ≡ x + fiso←1 : (x : A ∨ C) → fun←1 (fun→1 x) ≡ x fiso←1 (case1 a) = cong case1 (fiso← ab a) fiso←1 (case2 c) = cong case2 (fiso← cd c) @@ -238,8 +238,8 @@ -- nn zero = record { j = 0 ; k = 0 ; k1 = refl ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } - nn (suc i) with NN.k (nn i) | inspect NN.k (nn i) - ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 + nn (suc i) with NN.k (nn i) in eq + ... | zero = record { k = suc (sum ) ; j = 0 ; k1 = nn02 ; nn-unique = nn04 } where --- --- increment the stage @@ -283,7 +283,7 @@ i ∎ where open ≡-Reasoning nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ nn06 = NN.nn-unique (nn i) - ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where + ... | suc k = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where --- --- increment in a stage --- @@ -459,8 +459,8 @@ lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x lb05 x eq = lb=b [] x (sym eq) - lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) - ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where + lb (suc n) with LB.nlist (lb n) in eq + ... | [] = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where open ≡-Reasoning lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n lb10 = begin @@ -471,7 +471,7 @@ suc n ∎ lb06 : (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x - ... | false ∷ t | record { eq = eq } = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where + ... | false ∷ t = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where lb01 : lton (true ∷ t) ≡ suc n lb01 = begin lton (true ∷ t) ≡⟨ refl ⟩ @@ -482,7 +482,7 @@ suc n ∎ where open ≡-Reasoning lb09 : (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x - ... | true ∷ t | record { eq = eq } = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where + ... | true ∷ t = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where lb03 : lton (true ∷ t) ≡ n lb03 = begin lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ @@ -535,55 +535,55 @@ record IsImage0 (A B : Set ) (f : (x : A ) → B) (x : B ) : Set where field y : A - x=fy : x ≡ f y + x=fy : x ≡ f y -IsImage : (a b : Set) (iab : InjectiveF a b ) (x : b ) → Set +IsImage : (a b : Set) (iab : InjectiveF a b ) (x : b ) → Set IsImage a b iab x = IsImage0 a b (InjectiveF.f iab) x -Bernstein : (A B : Set) - → (fi : InjectiveF A B ) → (gi : InjectiveF B A ) - → (is-A : (b : B ) → Dec (Is A B (InjectiveF.f fi) b) ) - → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f gi) a) ) - → Bijection A B -Bernstein A B fi gi isa isb = ? where - open InjectiveF - gfi : InjectiveF A A - gfi = record { f = λ x → f gi (f fi x) ; inject = λ {x} {y} eq → inject fi (inject gi eq) } - data gfImage : (x : A) → Set where - a-g : {x : A} → (¬ib : ¬ ( IsImage B A gi x )) → gfImage x - next-gf : {x : A} → (ix : IsImage A A gfi x) → (gfiy : gfImage (IsImage0.y ix) ) → gfImage x - data ¬gfImage : (x : A) → Set where - ngf : {x : A} → (¬gfiy : ¬ gfImage x) → ¬gfImage x - gf02 : {x : A} → IsImage B A gi x ∨ (¬ IsImage B A gi x) ∨ ((ix : IsImage A A gfi x) → ¬ gfImage (IsImage0.y ix) ) → ¬ gfImage x - gf02 {x} c gf = ? - gfi∨ : (x : A) → gfImage x ∨ ¬gfImage x - gfi∨ x with isb x - ... | no ¬ib = case1 ( a-g (λ ib → ¬ib (record { a = IsImage0.y ib ; fa=c = sym (IsImage0.x=fy ib) }))) - ... | yes ib with isa (f fi x) - ... | no ¬ia = case2 ( ngf ? ) - ... | yes ia = case1 ( next-gf record { y = f gi (Is.a ib) ; x=fy = br00 } (a-g br01 ) ) where - br00 : x ≡ f gi (f fi (f gi (Is.a ib))) - br00 = ? - br01 : ¬ IsImage B A gi (f gi (Is.a ib)) - br01 record { y = y ; x=fy = x=fy } = ? +-- Bernstein : (A B : Set) +-- → (fi : InjectiveF A B ) → (gi : InjectiveF B A ) +-- → (is-A : (b : B ) → Dec (Is A B (InjectiveF.f fi) b) ) +-- → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f gi) a) ) +-- → Bijection A B +-- Bernstein A B fi gi isa isb = ? where +-- open InjectiveF +-- gfi : InjectiveF A A +-- gfi = record { f = λ x → f gi (f fi x) ; inject = λ {x} {y} eq → inject fi (inject gi eq) } +-- data gfImage : (x : A) → Set where +-- a-g : {x : A} → (¬ib : ¬ ( IsImage B A gi x )) → gfImage x +-- next-gf : {x : A} → (ix : IsImage A A gfi x) → (gfiy : gfImage (IsImage0.y ix) ) → gfImage x +-- data ¬gfImage : (x : A) → Set where +-- ngf : {x : A} → (¬gfiy : ¬ gfImage x) → ¬gfImage x +-- gf02 : {x : A} → IsImage B A gi x ∨ (¬ IsImage B A gi x) ∨ ((ix : IsImage A A gfi x) → ¬ gfImage (IsImage0.y ix) ) → ¬ gfImage x +-- gf02 {x} c gf = ? +-- gfi∨ : (x : A) → gfImage x ∨ ¬gfImage x +-- gfi∨ x with isb x +-- ... | no ¬ib = case1 ( a-g (λ ib → ¬ib (record { a = IsImage0.y ib ; fa=c = sym (IsImage0.x=fy ib) }))) +-- ... | yes ib with isa (f fi x) +-- ... | no ¬ia = case2 ( ngf ? ) +-- ... | yes ia = case1 ( next-gf record { y = f gi (Is.a ib) ; x=fy = br00 } (a-g br01 ) ) where +-- br00 : x ≡ f gi (f fi (f gi (Is.a ib))) +-- br00 = ? +-- br01 : ¬ IsImage B A gi (f gi (Is.a ib)) +-- br01 record { y = y ; x=fy = x=fy } = ? Countable-Bernstein : (A B C : Set) → Bijection A ℕ → Bijection C ℕ → (fi : InjectiveF A B ) → (gi : InjectiveF B C ) - → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) + → (is-A : (c : C ) → Dec (Is A C (λ x → (InjectiveF.f gi (InjectiveF.f fi x))) c )) → (is-B : (c : C ) → Dec (Is B C (InjectiveF.f gi) c) ) → Bijection B ℕ Countable-Bernstein A B C an cn fi gi is-A is-B = record { fun→ = λ x → bton x ; fun← = λ n → ntob n ; fiso→ = biso - ; fiso← = biso1 + ; fiso← = biso1 } where -- -- an f g cn -- ℕ ↔ A → B → C ↔ ℕ -- B = Image A f ∪ (B \ Image A f ) - -- + -- open Bijection f = InjectiveF.f fi g = InjectiveF.f gi @@ -646,7 +646,7 @@ c-mono : (i j : ℕ ) → i ≤ j → c i ≤ c j c-mono i j i≤j with ≤-∨ i≤j ... | case1 refl = ≤-refl - c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j) + c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j) c-mono (suc i) (suc j) (s≤s i≤j) | case2 (s≤s lt) = ≤-trans (c-mono (suc i) j lt ) (c-mono1 j) inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j @@ -693,7 +693,7 @@ lem02 zero (h ∷ t) refl with is-A (fun← cn zero) ... | yes _ = refl ... | no _ = refl - lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n)) + lem02 (suc n) (h ∷ t) refl with is-A (fun← cn (suc n)) ... | yes _ = cong suc (lem02 n t refl) ... | no _ = lem02 n t refl @@ -705,7 +705,7 @@ -- count of a in a-list is one step reduced -- - a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) + a-list-ca : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) → suc (ca-list (a-list i cl a)) ≡ ca-list cl a-list-ca i cl a = lem03 i cl _ a refl where lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) → cal ≡ (a-list i cl a) → suc (ca-list cal) ≡ ca-list cl @@ -721,13 +721,13 @@ -- reduced list still have all ani j < i -- - a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) - → (j : ℕ) → j < i → Any (_≡_ (g (f (fun← an j)))) cl → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a) + a-list-any : (i : ℕ) → (cl : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) + → (j : ℕ) → j < i → Any (_≡_ (g (f (fun← an j)))) cl → Any (_≡_ (g (f (fun← an j)))) (a-list i cl a) a-list-any i cl a j j<i b = lem03 i cl _ a refl j j<i b where - lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) - → cal ≡ (a-list i cl a) + lem03 : (i : ℕ) → (cl cal : List C) → (a : Any (_≡_ (g (f (fun← an i)))) cl ) + → cal ≡ (a-list i cl a) → (j : ℕ) → j < i → Any (_≡_ (g (f (fun← an j)))) cl → Any (_≡_ (g (f (fun← an j)))) cal - lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡< + lem03 i (h ∷ t) cal (here px) eq j j<i (here px₁) = ⊥-elim ( nat-≡< ( bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) j<i ) lem03 i (h ∷ t) cal (here px) eq j j<i (there b) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b lem03 i (h ∷ t) cal (there a) eq j j<i (here px) = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) (here px) @@ -745,14 +745,14 @@ -- del : (i : ℕ) → (cl : List C) → any-cl i cl → List C -- del 0 contains ani 0 - del i cl a = a-list i cl (a i ≤-refl) + del i cl a = a-list i cl (a i ≤-refl) del-any : (i : ℕ) → (cl : List C) → (a : any-cl (suc i) cl) → any-cl i (del (suc i) cl a ) del-any i cl a j le = lem41 cl (del (suc i) cl a ) (a (suc i) ≤-refl ) (a j (≤-trans le a≤sa) ) refl where - lem41 : (cl dl : List C) + lem41 : (cl dl : List C) → (ai : Any (_≡_ (g (f (fun← an (suc i))))) cl) - → (aj : Any (_≡_ (g (f (fun← an j)))) cl) + → (aj : Any (_≡_ (g (f (fun← an j)))) cl) → dl ≡ a-list (suc i) cl ai → Any (_≡_ (g (f (fun← an j)))) dl - lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡< + lem41 (h ∷ t) y (here px) (here px₁) eq = ⊥-elim ( nat-≡< ( bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi (trans px₁ (sym px))))) (x≤y→x<sy le) ) lem41 (h ∷ t) y (here px) (there b0) eq = subst (λ k → Any (_≡_ (g (f (fun← an j)))) k) (sym eq) b0 lem41 (h ∷ t) y (there a0) (here px) refl = here px @@ -760,17 +760,17 @@ del-ca : (i : ℕ) → (cl : List C) → (a : any-cl i cl ) → suc (ca-list (del i cl a)) ≡ ca-list cl - del-ca i cl a = a-list-ca i cl (a i ≤-refl) + del-ca i cl a = a-list-ca i cl (a i ≤-refl) lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl lem30 0 cl i≤n a = begin - 1 ≤⟨ s≤s z≤n ⟩ + 1 ≤⟨ s≤s z≤n ⟩ suc (ca-list (del 0 cl a) ) ≡⟨ del-ca 0 cl a ⟩ ca-list cl ∎ where open ≤-Reasoning lem30 (suc i) cl i≤n a = begin - suc (suc i) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ - suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩ + suc (suc i) ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ + suc (ca-list (del (suc i) cl a)) ≡⟨ del-ca (suc i) cl a ⟩ ca-list cl ∎ where open ≤-Reasoning @@ -814,14 +814,14 @@ lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B i ≡ count-B j → i ≡ j lem06 i j bi bj eq = lem08 where lem20 : (i j : ℕ) → i < j → Is B C g (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥ - lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (suc j)) | inspect count-B (suc j) - ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) - ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) - ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where + lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) in eq1 | is-B (fun← cn (suc j)) in eq2 + ... | no nisc | _ = ⊥-elim (nisc bi) + ... | yes _ | no nisc = ⊥-elim (nisc bj) + ... | yes _ | yes _ = ⊥-elim ( nat-≤> lem25 a<sa) where lem22 : 1 ≡ count-B 0 - lem22 with is-B (fun← cn 0) | inspect count-B 0 - ... | yes _ | record { eq = eq1 } = refl - ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem22 with is-B (fun← cn 0) in eq1 + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa bi ) lem24 : count-B j ≡ 0 lem24 = cong pred le lem25 : 1 ≤ 0 @@ -837,18 +837,18 @@ -- cb i < suc (cb i) < cb (suc i) ≤ cb j -- suc (cb i) ≡ suc (cb j) → cb i ≡ cb j lem22 : suc (count-B i) ≡ count-B (suc i) - lem22 with is-B (fun← cn (suc i)) | inspect count-B (suc i) - ... | yes _ | record { eq = eq1 } = refl - ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem22 with is-B (fun← cn (suc i)) in eq1 + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa bi ) lem23 : suc (count-B j) ≡ count-B (suc j) - lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j) - ... | yes _ | record { eq = eq1 } = refl - ... | no nisa | _ = ⊥-elim ( nisa bj ) + lem23 with is-B (fun← cn (suc j)) in eq1 + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa bj ) lem24 : count-B i ≡ count-B j - lem24 with is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (suc j)) | inspect count-B (suc j) - ... | no nisc | _ | _ | _ = ⊥-elim (nisc bi) - ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc bj) - ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le) + lem24 with is-B (fun← cn (suc i)) in eq1 | is-B (fun← cn (suc j)) in eq2 + ... | no nisc | _ = ⊥-elim (nisc bi) + ... | yes _ | no nisc = ⊥-elim (nisc bj) + ... | yes _ | yes _ = sym (cong pred le) lem21 : suc (count-B i) ≤ count-B j lem21 = begin suc (count-B i) ≡⟨ lem22 ⟩ @@ -861,33 +861,46 @@ ... | tri≈ ¬a b ¬c = b ... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq ) + lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n - lem07 n 0 eq with is-B (fun← cn 0) | inspect count-B 0 - ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq - ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem07 n 0 eq with is-B (fun← cn 0) + ... | yes isb = lem13 where + cb1 = count-B 0 + lem14 : count-B 0 ≡ 1 + lem14 with is-B (fun← cn 0) + ... | yes _ = refl + ... | no ne = ⊥-elim (ne isb) lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → 1 ≡ count-B cb1 → 0 ≡ cb1 - lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq) - ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) - lem07 n (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i) - ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq - ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq) } where + lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans lem14 cbeq) + lem13 : CountB n + lem13 = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) } + ... | no nisb = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) + lem07 n (suc i) eq with is-B (fun← cn (suc i)) + ... | yes isb = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) } where + cbs = count-B (suc i) + lem14 : count-B (suc i) ≡ suc (count-B i) + lem14 with is-B (fun← cn (suc i)) + ... | yes _ = refl + ... | no ne = ⊥-elim (ne isb) lem12 : (cb1 : ℕ) → Is B C g (fun← cn cb1) → suc (count-B i) ≡ count-B cb1 → suc i ≡ cb1 - lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq) - ... | no nisb | record { eq = eq1 } = lem07 n i eq + lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans lem14 cbeq) + ... | no nisb = lem07 n i eq -- starting from 0, if count B i ≡ suc n, this is it lem09 : (i j : ℕ) → suc n ≤ j → j ≡ count-B i → CountB n lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le) ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq )) - ... | case2 (s≤s lt) with is-B (fun← cn 0) | inspect count-B 0 - ... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) - ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n)) + ... | case2 (s≤s lt) with is-B (fun← cn 0) in eq1 + ... | yes isb = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) + ... | no nisb = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n)) lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le) ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq )) - ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) | inspect count-B (suc i) - ... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq) - ... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq + ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) in eq1 + ... | yes isb = lem09 i j lt (cong pred eq) + ... | no nisb = lem09 i (suc j) (≤-trans lt a≤sa) eq bton : B → ℕ bton b = pred (count-B (fun→ cn (g b))) @@ -896,7 +909,7 @@ ntob n = CountB.b (lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )) biso : (n : ℕ) → bton (ntob n) ≡ n - biso n = begin + biso n = begin bton (ntob n) ≡⟨ refl ⟩ pred (count-B (fun→ cn (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (fun→ cn k))) ( CountB.b=cn CB)) ⟩ pred (count-B (fun→ cn (fun← cn (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (fiso→ cn _) ⟩ @@ -910,18 +923,18 @@ -- uniqueness of ntob is proved by injection -- biso1 : (b : B) → ntob (bton b) ≡ b - biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) - ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where + biso1 b with count-B (fun→ cn (g b)) in eq1 + ... | zero = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero lem20 = eq1 lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B i - lem21 0 eq with is-B (fun← cn 0) | inspect count-B 0 - ... | yes isb | record { eq = eq1 } = ≤-refl - ... | no nisb | record{ eq = eq1 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) - lem21 (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i) - ... | yes isb | record{ eq = eq2 } = s≤s z≤n - ... | no nisb | record{ eq = eq2 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) - ... | suc n | record { eq = eq1 } = begin + lem21 0 eq with is-B (fun← cn 0) in eq1 + ... | yes isb = ≤-refl + ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) + lem21 (suc i) eq with is-B (fun← cn (suc i)) in eq1 + ... | yes isb = s≤s z≤n + ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) + ... | suc n = begin CountB.b CB ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩ fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩ @@ -1031,7 +1044,7 @@ ... | yes y = yes record { a = just h ∷ Is.a y ; fa=c = cong₂ (λ j k → ⟪ h ∷ j , true ∷ k ⟫ ) (cong proj1 (Is.fa=c y)) (cong proj2 (Is.fa=c y)) } ... | no n = no lem00 where lem00 : ¬ Is (List (Maybe A)) (List A ∧ List Bool) g ⟪ h ∷ t , true ∷ bt ⟫ - lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl } + lem00 record { a = (just x ∷ a) ; fa=c = refl } = n record { a = a ; fa=c = refl } dec1 ⟪ h ∷ t , false ∷ bt ⟫ with dec1 ⟪ h ∷ t , bt ⟫ ... | yes record { a = a ; fa=c = fa=c } = yes record { a = nothing ∷ a ; fa=c = cong₂ (λ j k → ⟪ j , false ∷ k ⟫) (cong proj1 fa=c) (cong proj2 fa=c) } ... | no n = no lem00 where @@ -1051,7 +1064,7 @@ -- just true ∷ just true ∷ nothing ∷ just true ∷ just true ∷ nothing ∷ just true ∷ nothing ∷ [] -- -- LBBℕ : Bijection (List (List Bool)) ℕ --- +-- -- Lℕ=ℕ : Bijection (List ℕ) ℕ --
--- a/src/cardinal.agda Sat Jun 22 12:39:58 2024 +0900 +++ b/src/cardinal.agda Sat Jun 22 19:23:56 2024 +0900 @@ -1,44 +1,71 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} +open import Level +open import Ordinals +open import logic +open import Relation.Nullary -open import Level hiding (suc ; zero ) +open import Level open import Ordinals -module cardinal {n : Level } (O : Ordinals {n}) where +import HODBase +import OD +open import Relation.Nullary +module cardinal {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) + (AC : OD.AxiomOfChoice O HODAxiom ) where + + +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Data.Empty + +import OrdUtil + +open Ordinals.Ordinals O +open Ordinals.IsOrdinals isOrdinal +import ODUtil open import logic --- import OD -import OD - -import ODC -open import Data.Nat -open import Relation.Binary.PropositionalEquality -open import Data.Nat.Properties -open import Data.Empty -open import Relation.Nullary -open import Relation.Binary -open import Relation.Binary.Core +open import nat -open inOrdinal O -open OD O -open OD.OD -open ODAxiom odAxiom -open import ZProduct O - -import OrdUtil -import ODUtil -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal --- open Ordinals.IsNext isNext open OrdUtil O -open ODUtil O - -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +open ODUtil O HODAxiom ho< open _∧_ open _∨_ open Bool -open _==_ + +open HODBase._==_ + +open HODBase.ODAxiom HODAxiom +open OD O HODAxiom + +open HODBase.HOD + +open AxiomOfChoice AC +open import ODC O HODAxiom AC as ODC + +open import Level +open import Ordinals + +import filter -open HOD +open import Relation.Nullary +-- open import Relation.Binary hiding ( _⇔_ ) +open import Data.Empty +open import Relation.Binary.PropositionalEquality +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +import BAlgebra + +-- open BAlgebra O +open import ZProduct O HODAxiom ho< + + +------- +-- the set of finite partial functions from ω to 2 +-- +-- + +open import Data.List hiding (filter) +open import Data.Maybe + -- record HODBijection (A B : HOD ) : Set n where -- field @@ -49,7 +76,7 @@ -- fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x -- fiso← : (x : Ordinal ) → ( lt : odef B x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x -open Injection +open Injection -- in ZProduct open HODBijection record IsImage0 (a b : HOD) (f : (x : Ordinal) → odef a x → Ordinal) (x : Ordinal ) : Set n where @@ -59,7 +86,7 @@ x=fy : x ≡ f y ay IsImage : (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) → Set n -IsImage a b iab x = IsImage0 (* a) (* b) (i→ iab) x +IsImage a b iab x = IsImage0 (* a) (* b) (λ x ax → i→ iab x) x Image : (a : Ordinal) { b : Ordinal } → Injection a b → HOD Image a {b} iab = record { od = record { def = λ x → IsImage a b iab x } ; odmax = b ; <odmax = im00 } where @@ -78,23 +105,37 @@ open import BAlgebra O -_-_ : (a b : Ordinal ) → Ordinal -a - b = & ( (* a) ＼ (* b) ) - --→< : (a b : Ordinal ) → (a - b) o≤ a --→< a b = subst₂ (λ j k → j o≤ k) &iso &iso ( ⊆→o≤ ( λ {x} a-b → proj1 (subst ( λ k → odef k x) *iso a-b) ) ) - -b-a⊆b : {a b x : Ordinal } → odef (* (b - a)) x → odef (* b) x -b-a⊆b {a} {b} {x} lt with subst (λ k → odef k x) *iso lt -... | ⟪ bx , ¬ax ⟫ = bx +b-a⊆b : {a b x : Ordinal } → odef ((* b) ＼ (* a)) x → odef (* b) x +b-a⊆b {a} {b} {x} ⟪ bx , nax ⟫ = bx Injection-⊆ : {a b c : Ordinal } → * c ⊆ * a → Injection a b → Injection c b -Injection-⊆ {a} {b} {c} le f = record { i→ = λ x cx → i→ f x (le cx) ; iB = λ x cx → iB f x (le cx) - ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq } +Injection-⊆ {a} {b} {c} le f = record { i→ = λ x → i→ f x ; iB = λ x cx → iB f x (le cx) + ; inject = λ x y ix iy eq → inject f x y (le ix) (le iy) eq } Injection-∙ : {a b c : Ordinal } → Injection a b → Injection b c → Injection a c -Injection-∙ {a} {b} {c} f g = record { i→ = λ x ax → i→ g (i→ f x ax) (iB f x ax) ; iB = λ x ax → iB g (i→ f x ax) (iB f x ax) - ; inject = λ x y ix iy eq → inject f x y ix iy (inject g (i→ f x ix) (i→ f y iy) (iB f x ix) (iB f y iy) eq) } +Injection-∙ {a} {b} {c} f g = record { i→ = λ x → i→ g (i→ f x ) ; iB = λ x ax → iB g (i→ f x ) (iB f x ax) + ; inject = λ x y ix iy eq → inject f _ _ ix iy (inject g _ _ (iB f x ix ) (iB f y iy ) eq ) } + +==-bi : {A B C : HOD } → (ab : HODBijection A B) + → ( (x : Ordinal ) → ( lt1 lt2 : odef A x ) → fun→ ab x lt1 ≡ fun→ ab x lt2 ) + → ( (x : Ordinal ) → ( lt1 lt2 : odef B x ) → fun← ab x lt1 ≡ fun← ab x lt2 ) + → (A =h= C → HODBijection C B) ∧ (B =h= C → HODBijection A C) +proj1 (==-bi {A} {B} {C} ab wld→ wld← ) a=c = record { + fun→ = λ x cx → fun→ ab x (eq← a=c cx) + ; fun← = λ x bx → fun← ab x bx + ; funB = λ x cx → funB ab x (eq← a=c cx) + ; funA = λ x cx → eq→ a=c (funA ab x cx) + ; fiso→ = λ x bx → trans (wld→ _ _ _) (fiso→ ab x bx) + ; fiso← = λ x cx → fiso← ab x (eq← a=c cx) + } +proj2 (==-bi {A} {B} {C} ab wld→ wld←) b=c = record { + fun→ = λ x cx → fun→ ab x cx + ; fun← = λ x bx → fun← ab x (eq← b=c bx) + ; funB = λ x cx → eq→ b=c (funB ab x cx) + ; funA = λ x cx → funA ab x (eq← b=c cx) + ; fiso→ = λ x cx → fiso→ ab x (eq← b=c cx) + ; fiso← = λ x bx → trans (wld← _ _ _) (fiso← ab x bx) + } -- -- Two injection can be joined @@ -139,10 +180,10 @@ Bernstein : {a b : Ordinal } → Injection a b → Injection b a → HODBijection (* a) (* b) Bernstein {a} {b} ( fi @ record { i→ = f ; iB = b∋f ; inject = f-inject }) ( gi @ record { i→ = g ; iB = a∋g ; inject = g-inject }) - = subst₂ (λ j k → HODBijection j k ) (sym a=UC∨a-UC) (sym b=fUC∨b-fUC) (bi-∪ bi-UC bi-fUC) + = proj1 (==-bi (proj2 (==-bi (bi-∪ bi-UC bi-fUC) ? ? ) (==-sym b=fUC∨b-fUC)) ? ? ) (==-sym a=UC∨a-UC) where gf : Injection a a - gf = record { i→ = λ x ax → g (f x ax) (b∋f x ax) ; iB = λ x ax → a∋g _ (b∋f x ax) + gf = record { i→ = λ x → g (f x ) ; iB = λ x ax → a∋g _ (b∋f x ax) ; inject = λ x y ax ay eq → f-inject _ _ ax ay ( g-inject _ _ (b∋f _ ax) (b∋f _ ay) eq) } -- HOD UC is closure of gi ∙ fi starting from a - Image g @@ -179,18 +220,21 @@ a-UC = record { od = record { def = λ x → odef (* a) x ∧ (¬ gfImage x) } ; odmax = & (* a) ; <odmax = λ lt → odef< (proj1 lt) } - a=UC∨a-UC : * a ≡ UC ∪ a-UC - a=UC∨a-UC = ==→o≡ record { eq→ = be00 ; eq← = be01 } where + a=UC∨a-UC : (* a) =h= (UC ∪ a-UC) + a=UC∨a-UC = record { eq→ = be00 ; eq← = be01 } where be00 : {x : Ordinal} → odef (* a) x → odef (UC ∪ a-UC) x - be00 {x} ax with ODC.p∨¬p O ( gfImage x) + be00 {x} ax with p∨¬p ( gfImage x) ... | case1 gfx = case1 gfx ... | case2 ngfx = case2 ⟪ ax , ngfx ⟫ be01 : {x : Ordinal} → odef (UC ∪ a-UC) x → odef (* a) x be01 {x} (case1 gfx) = a∋gfImage gfx be01 {x} (case2 ngfx) = proj1 ngfx + wld-a : (x : Ordinal) (lt1 lt2 : odef (UC ∪ a-UC) x) → ? -- fa bi-UC bi-fUC x lt1 ≡ fa bi-UC bi-fUC x lt2 + wld-a = ? + FA : (x : Ordinal) → (ax : gfImage x) → Ordinal - FA x ax = f x (a∋gfImage ax) + FA x ax = f x -- (a∋gfImage ax) b∋f⁻¹ : (x : Ordinal) → IsImage0 UC (* b) FA x → odef (* b) x b∋f⁻¹ x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋f y (a∋gfImage ay)) @@ -201,10 +245,10 @@ b-fUC : HOD b-fUC = record { od = record { def = λ x → odef (* b) x ∧ (¬ IsImage0 UC (* b) FA x) } ; odmax = & (* b) ; <odmax = λ lt → odef∧< lt } - b=fUC∨b-fUC : * b ≡ fUC ∪ b-fUC - b=fUC∨b-fUC = ==→o≡ record { eq→ = be00 ; eq← = be01 } where + b=fUC∨b-fUC : * b =h= (fUC ∪ b-fUC) + b=fUC∨b-fUC = record { eq→ = be00 ; eq← = be01 } where be00 : {x : Ordinal} → odef (* b) x → odef (fUC ∪ b-fUC) x - be00 {x} bx with ODC.p∨¬p O (IsImage0 UC (* b) FA x) + be00 {x} bx with p∨¬p (IsImage0 UC (* b) FA x) ... | case1 gfx = case1 gfx ... | case2 ngfx = case2 ⟪ bx , ngfx ⟫ be01 : {x : Ordinal} → odef (fUC ∪ b-fUC) x → odef (* b) x @@ -212,15 +256,15 @@ be01 {x} (case2 ngfx) = proj1 ngfx nimg : {x : Ordinal } → (ax : odef (* a) x ) → ¬ (odef UC x) → IsImage b a gi x - nimg {x} ax ncn with ODC.p∨¬p O (IsImage b a gi x) + nimg {x} ax ncn with p∨¬p (IsImage b a gi x) ... | case1 img = img ... | case2 nimg = ⊥-elim ( ncn (a-g ax nimg ) ) - f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → f x ax ≡ f y ax1 - f-cong {x} {x} {ax} {ax1} refl = cong (λ k → f x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) + f-cong : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → f x ≡ f y + f-cong {x} {x} {ax} {ax1} refl = ? -- cong (λ k → f x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) - g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y} → x ≡ y → g x bx ≡ g y bx1 - g-cong {x} {x} {bx} {bx1} refl = cong (λ k → g x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 )) + g-cong : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y} → x ≡ y → g x ≡ g y + g-cong {x} {x} {bx} {bx1} refl = ? -- cong (λ k → g x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 )) g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → Ordinal g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = y @@ -228,10 +272,10 @@ b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) (nc0 : IsImage b a gi x ) → odef (* b) (g⁻¹ ax nc0) b∋g⁻¹ {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = ay - g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → g (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x + g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : IsImage b a gi x ) → g (g⁻¹ ax nc0) ≡ x g⁻¹-iso {x} ax record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy - g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a gi (g x bx) ) → g⁻¹ (a∋g x bx) nc0 ≡ x + g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a gi (g x ) ) → g⁻¹ (a∋g x bx) nc0 ≡ x g⁻¹-iso1 {x} bx nc0 = inject gi _ _ (b∋g⁻¹ (a∋g x bx) nc0) bx (g⁻¹-iso (a∋g x bx) nc0) g⁻¹-eq : {x : Ordinal } → (ax ax' : odef (* a) x) → {nc0 nc0' : IsImage b a gi x } → g⁻¹ ax nc0 ≡ g⁻¹ ax' nc0' @@ -240,25 +284,25 @@ cc11-case2 : {x : Ordinal} (ax : odef (* a) x) → (ncn : ¬ gfImage x) - → ¬ IsImage0 UC (* b) (λ x ax → f x (a∋gfImage ax)) (g⁻¹ ax (nimg ax ncn)) + → ¬ IsImage0 UC (* b) (λ x ax → f x ) (g⁻¹ ax (nimg ax ncn)) cc11-case2 {x} ax ncn record { y = y ; ay = ay ; x=fy = x=fy } with nimg ax ncn ... | record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } = ncn ( subst (λ k → gfImage k) be113 (next-gf record { y = y ; ay = (a∋gfImage ay) ; x=fy = refl } ay ) ) where - be113 : g (f y (a∋gfImage ay)) (b∋f y (a∋gfImage ay)) ≡ x + be113 : g (f y ) ≡ x be113 = begin - g (f y (a∋gfImage ay)) (b∋f y (a∋gfImage ay)) ≡⟨ g-cong (sym x=fy) ⟩ - g y1 ay1 ≡⟨ sym (x=fy1) ⟩ + g (f y ) ≡⟨ g-cong (sym x=fy) ⟩ + g y1 ≡⟨ sym (x=fy1) ⟩ x ∎ where open ≡-Reasoning cc10-case2 : {x : Ordinal } → (bx : odef (* b) x ) - → ¬ IsImage0 UC (* b) (λ x ax → f x (a∋gfImage ax)) x - → ¬ gfImage (g x bx) + → ¬ IsImage0 UC (* b) (λ x ax → f x ) x + → ¬ gfImage (g x ) cc10-case2 {x} bx nix (a-g ax ¬ib) = ¬ib record { y = _ ; ay = bx ; x=fy = refl } cc10-case2 {x} bx nix (next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfy) = nix record { y = _ ; ay = gfy ; x=fy = inject gi _ _ bx (b∋f y (a∋gfImage gfy)) (trans x=fy (g-cong (f-cong refl))) } fU1 : (x : Ordinal) → odef UC x → Ordinal - fU1 x gfx = f x (a∋gfImage gfx) + fU1 x gfx = f x f⁻¹ : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal f⁻¹ x record { y = y ; ay = ay ; x=fy = x=fy } = y @@ -277,7 +321,7 @@ bi-UC : HODBijection UC fUC bi-UC = record { - fun→ = λ x lt → f x (a∋gfImage lt) + fun→ = λ x lt → f x ; fun← = λ x lt → f⁻¹ x lt ; funB = λ x lt → record { y = _ ; ay = lt ; x=fy = refl } ; funA = λ x lt → UC∋f⁻¹ lt @@ -288,21 +332,21 @@ b-FUC∋g⁻¹ : {x : Ordinal } → (lt : odef a-UC x )→ odef b-fUC (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) b-FUC∋g⁻¹ {x} ⟪ ax , ngfix ⟫ = ⟪ b∋g⁻¹ ax (nimg ax ngfix) , cc11-case2 ax ngfix ⟫ - a-UC∋g : {x : Ordinal } → (lt : odef b-fUC x) → odef a-UC (g x (proj1 lt )) + a-UC∋g : {x : Ordinal } → (lt : odef b-fUC x) → odef a-UC (g x ) a-UC∋g {x} ⟪ bx , ¬img ⟫ = ⟪ a∋g x bx , cc10-case2 bx ¬img ⟫ fUC-iso1 : {x : Ordinal } → (lt : odef b-fUC x ) → g⁻¹ (proj1 (a-UC∋g lt)) (nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt))) ≡ x fUC-iso1 {x} lt with nimg (proj1 (a-UC∋g lt)) (proj2 (a-UC∋g lt)) ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject gi _ _ (proj1 lt) ay x=fy ) - fUC-iso0 : {x : Ordinal} → (lt : odef a-UC x) → g (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) (proj1 (b-FUC∋g⁻¹ lt)) ≡ x + fUC-iso0 : {x : Ordinal} → (lt : odef a-UC x) → g (g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt))) ≡ x fUC-iso0 {x} lt with nimg (proj1 lt) (proj2 lt) ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy bi-fUC : HODBijection a-UC b-fUC bi-fUC = record { fun→ = λ x lt → g⁻¹ (proj1 lt) (nimg (proj1 lt) (proj2 lt)) - ; fun← = λ x lt → g x (proj1 lt) + ; fun← = λ x lt → g x ; funB = λ x lt → b-FUC∋g⁻¹ lt ; funA = λ x lt → a-UC∋g lt ; fiso→ = λ x lt → fUC-iso1 lt @@ -326,17 +370,17 @@ -- Cardinal⊆ = {!!} -- we may have infinite sets with the same cardinality PtoF : {u : HOD} {x s : Ordinal } → odef (Power u) s → odef u x → Bool -PtoF {u} {x} {s} su ux with ODC.p∨¬p O (odef (* s) x ) +PtoF {u} {x} {s} su ux with p∨¬p (odef (* s) x ) ... | case1 a = true ... | case2 b = false fun←cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef S x} {ax1 : odef S y} → x ≡ y → fun← b x ax ≡ fun← b y ax1 -fun←cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 )) +fun←cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun← b x k) ? -- ( HE.≅-to-≡ ( ∋-irr {S} ax ax1 )) fun→cong : {P S : HOD} (b : HODBijection P S ) {x y : Ordinal } → {ax : odef P x} {ax1 : odef P y} → x ≡ y → fun→ b x ax ≡ fun→ b y ax1 -fun→cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ( HE.≅-to-≡ ( ∋-irr {P} ax ax1 )) +fun→cong {P} {S} b {x} {x} {ax} {ax1} refl = cong (λ k → fun→ b x k) ? -- ( HE.≅-to-≡ ( ∋-irr {P} ax ax1 )) -- S @@ -347,29 +391,29 @@ Cantor1 : ( S : HOD ) → S c< Power S Cantor1 S f = diag4 where f1 : Injection (& S) (& (Power S)) - f1 = record { i→ = λ x sx → & (* x , * x) ; iB = c00 ; inject = c02 }where + f1 = record { i→ = λ x → & (* x , * x) ; iB = c00 ; inject = c02 }where c02 : (x y : Ordinal) (ltx : odef (* (& S)) x) (lty : odef (* (& S)) y) → & (* x , * x) ≡ & (* y , * y) → x ≡ y - c02 x y ltx lty eq = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (xx=zy→x=y c03 )) where + c02 x y ltx lty eq = ? where -- subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (xx=zy→x=y c03 )) where c03 : (* x , * x) =h= (* y , * y) c03 = ord→== eq c00 : (x : Ordinal) (lt : odef (* (& S)) x) → odef (* (& (Power S))) (& (* x , * x)) - c00 x lt = subst₂ (λ j k → odef j (& k) ) (sym *iso) refl (λ y z → c01 y (subst (λ k → odef k y ) *iso z )) where + c00 x lt = ? where -- subst₂ (λ j k → odef j (& k) ) (sym *iso) refl (λ y z → c01 y (subst (λ k → odef k y ) *iso z )) where c01 : (y : Ordinal ) → odef (* x , * x ) y → odef S y - c01 y (case1 eq) = subst₂ (λ j k → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt - c01 y (case2 eq) = subst₂ (λ j k → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt + c01 y (case1 eq) = ? --- subst₂ (λ j k → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt + c01 y (case2 eq) = ? -- subst₂ (λ j k → odef j k ) *iso (trans (sym &iso) (sym eq) ) lt f2 : Injection (& (Power S)) (& S) f2 = f - postulate -- yes we have a proof but it is very slow - b : HODBijection (Power S) S - -- b = subst₂ (λ j k → HODBijection j k) *iso *iso ( Bernstein f2 f1) -- this makes check very slow + -- postulate -- yes we have a proof but it is very slow + b : HODBijection (Power S) S + b = subst₂ (λ j k → HODBijection j k) ? ? ( Bernstein f2 f1) -- this makes check very slow -- but postulate makes check weak eg. irrerevance of ∋ -- we have at least one element since Power S contains od∅ -- p0 : odef (Power S) o∅ - p0 z xz = ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz) ) + p0 z xz = ? -- ⊥-elim (¬x<0 (subst (λ k → odef k z) o∅≡od∅ xz) ) s : Ordinal s = fun→ b o∅ p0 @@ -378,7 +422,7 @@ ss = funB b o∅ p0 is-S : (S : HOD) → (x : Ordinal ) → Bool - is-S S x with ODC.p∨¬p O (odef S x ) + is-S S x with p∨¬p (odef S x ) ... | case1 _ = true ... | case2 _ = false @@ -390,21 +434,21 @@ ; odmax = & S ; <odmax = odef∧< } diag3 : odef (Power S) (& Diag) - diag3 z xz with subst (λ k → odef k z) *iso xz - ... | ⟪ sx , eq ⟫ = sx + diag3 z xz = ? -- with subst (λ k → odef k z) *iso xz + -- ... | ⟪ sx , eq ⟫ = sx not-isD : (x : Ordinal) → (sn : odef S x) → not ( is-S (* (fun← b x sn )) x ) ≡ is-S Diag x - not-isD x sn with ODC.p∨¬p O (odef (* (fun← b x sn )) x) | ODC.p∨¬p O (odef Diag x) | inspect (is-S (* (fun← b x sn ))) x - ... | case1 lt | case1 ⟪ sx , eq ⟫ | record { eq = eq1 } = ⊥-elim (¬t=f false (trans (sym eq1) (eq sn )) ) - ... | case1 lt | case2 lt1 | _ = refl - ... | case2 lt | case1 lt1 | _ = refl - ... | case2 lt | case2 neg | record { eq = eq1 } = ⊥-elim ( neg ⟪ sn , (λ sx → trans (cong diag ( HE.≅-to-≡ ( ∋-irr {S} sx sn ))) eq1 ) ⟫ ) + not-isD x sn with p∨¬p (odef (* (fun← b x sn )) x) | p∨¬p (odef Diag x) | (is-S (* (fun← b x sn ))) x in eq1 + ... | case1 lt | case1 ⟪ sx , eq ⟫ | _ = ? -- ⊥-elim (¬t=f false (trans (sym eq1) (eq sn )) ) + ... | case1 lt | case2 lt1 | _ = ? + ... | case2 lt | case1 lt1 | _ = ? -- refl + ... | case2 lt | case2 neg | _ = ? --⊥-elim ( neg ⟪ sn , (λ sx → trans (cong diag ( HE.≅-to-≡ ( ∋-irr {S} sx sn ))) eq1 ) ⟫ ) diagn1 : (n : Ordinal ) → odef S n → ¬ (fun→ b (& Diag) diag3 ≡ n) diagn1 n sn dn = ¬t=f (is-S Diag n) (begin not (is-S Diag n) - ≡⟨ cong (λ k → not (is-S k n)) (sym *iso) ⟩ + ≡⟨ cong (λ k → not (is-S k n)) (sym ? ) ⟩ not (is-S (* (& Diag)) n) ≡⟨ cong (λ k → not (is-S (* k) n)) (sym (fiso← b (& Diag) diag3 )) ⟩ not ( is-S (* (fun← b (fun→ b (& Diag) diag3) (funB b (& Diag) diag3 ))) n ) @@ -419,11 +463,11 @@ diag4 = diagn1 (fun→ b (& Diag) diag3) (funB b (& Diag) diag3) refl c<¬= : { u s : HOD } → u c< s → ¬ ( u =c= s ) -c<¬= {u} {s} c<u ceq = c<u record { i→ = λ x lt → fun← ceq x (subst (λ k → odef k x) *iso lt) - ; iB = λ x lt → subst₂ (λ j k → odef j k) (sym *iso) refl (funA ceq x (subst (λ k → odef k x) *iso lt)) +c<¬= {u} {s} c<u ceq = c<u record { i→ = λ x → fun← ceq x (subst (λ k → odef k x) ? ?) + ; iB = λ x lt → subst₂ (λ j k → odef j k) (sym ?) refl (funA ceq x (subst (λ k → odef k x) ? lt)) ; inject = c04 } where c04 : (x y : Ordinal) (ltx : odef (* (& (s))) x) (lty : odef (* (& (s))) y) - → fun← ceq x (subst (λ k → odef k x) *iso ltx) ≡ fun← ceq y (subst (λ k → odef k y) *iso lty) → x ≡ y + → fun← ceq x (subst (λ k → odef k x) ? ltx) ≡ fun← ceq y (subst (λ k → odef k y) ? lty) → x ≡ y c04 x y ltx lty eq = begin x ≡⟨ sym ( fiso→ ceq x c05 ) ⟩ fun→ ceq ( fun← ceq x c05 ) (funA ceq x c05) ≡⟨ fun←cong (hodbij-sym ceq) eq ⟩ @@ -431,9 +475,9 @@ y ∎ where open ≡-Reasoning c05 : odef (s) x - c05 = subst (λ k → odef k x) *iso ltx + c05 = subst (λ k → odef k x) ? ltx c06 : odef (s) y - c06 = subst (λ k → odef k y) *iso lty + c06 = subst (λ k → odef k y) ? lty Cantor2 : (u : HOD) → ¬ ( u =c= Power u ) Cantor2 u = c<¬= (Cantor1 u )
--- a/src/partfunc.agda Sat Jun 22 12:39:58 2024 +0900 +++ b/src/partfunc.agda Sat Jun 22 19:23:56 2024 +0900 @@ -1,33 +1,72 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} +open import Level +open import Ordinals +open import logic +open import Relation.Nullary + open import Level -open import Relation.Nullary -open import Relation.Binary.PropositionalEquality --- open import Ordinals -module partfunc {n : Level } where -- (O : Ordinals {n}) where +open import Ordinals +import HODBase +import OD +open import Relation.Nullary +module partfunc {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) where + +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Data.Empty + +import OrdUtil + +open Ordinals.Ordinals O +open Ordinals.IsOrdinals isOrdinal +import ODUtil open import logic -open import Relation.Binary -open import Data.Empty -open import Data.Unit using ( ⊤ ; tt ) -open import Data.List hiding (filter) -open import Data.Maybe -open import Relation.Binary -open import Relation.Binary.Core -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) --- open import filter O +open import nat + +open OrdUtil O +open ODUtil O HODAxiom ho< open _∧_ open _∨_ open Bool +open HODBase._==_ + +open HODBase.ODAxiom HODAxiom +open OD O HODAxiom + +open HODBase.HOD + + +open import Relation.Nullary +open import Relation.Binary +open import Data.Empty +open import Relation.Binary +open import Relation.Binary.Core +open import Relation.Binary.PropositionalEquality +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) + +open import Data.Empty +open import Data.Unit using ( ⊤ ; tt ) +open import Data.List hiding (filter ; find) +open import Data.Maybe + +open _∧_ +open _∨_ +open Bool + +data Two : Set where + i0 : Two + i1 : Two + ---- -- -- Partial Function without ZF -- -record PFunc (Dom : Set n) (Cod : Set n) : Set (suc n) where +record PFunc {n m l : Level } (Dom : Set n) (Cod : Set m) : Set (suc (n ⊔ m ⊔ l)) where field - dom : Dom → Set n + dom : Dom → Set l pmap : (x : Dom ) → dom x → Cod meq : {x : Dom } → { p q : dom x } → pmap x p ≡ pmap x q @@ -36,26 +75,26 @@ -- PFunc (Lift n Nat) Cod is equivalent to List (Maybe Cod) -- -data Findp : {Cod : Set n} → List (Maybe Cod) → (x : Nat) → Set where - v0 : {Cod : Set n} → {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero - vn : {Cod : Set n} → {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) +data Findp {n : Level} {Cod : Set n} : List (Maybe Cod) → (x : Nat) → Set (suc n) where + v0 : {f : List (Maybe Cod)} → ( v : Cod ) → Findp ( just v ∷ f ) Zero + vn : {f : List (Maybe Cod)} {d : Maybe Cod} → {x : Nat} → Findp f x → Findp (d ∷ f) (Suc x) open PFunc -find : {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod +find : {n : Level} {Cod : Set n} → (f : List (Maybe Cod) ) → (x : Nat) → Findp f x → Cod find (just v ∷ _) 0 (v0 v) = v find (_ ∷ n) (Suc i) (vn p) = find n i p -findpeq : {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q +findpeq : {n : Level} {Cod : Set n} → (f : List (Maybe Cod)) → {x : Nat} {p q : Findp f x } → find f x p ≡ find f x q findpeq n {0} {v0 _} {v0 _} = refl findpeq [] {Suc x} {()} findpeq (just x₁ ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} findpeq (nothing ∷ n) {Suc x} {vn p} {vn q} = findpeq n {x} {p} {q} -List→PFunc : {Cod : Set n} → List (Maybe Cod) → PFunc (Lift n Nat) Cod -List→PFunc fp = record { dom = λ x → Lift n (Findp fp (lower x)) +List→PFunc : {Cod : Set (suc n)} → List (Maybe Cod) → PFunc (Lift n Nat) Cod +List→PFunc fp = record { dom = λ x → Lift zero (Findp fp (lower x)) ; pmap = λ x y → find fp (lower x) (lower y) - ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} + ; meq = λ {x} {p} {q} → findpeq fp {lower x} {lower p} {lower q} } ---- --