Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/cardinal.agda @ 1394:873924d06ff7
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 27 Jun 2023 09:20:55 +0900 |
parents | c67ecdf89e77 |
children | e39c2bffb86e |
line wrap: on
line source
{-# OPTIONS --allow-unsolved-metas #-} open import Level hiding (suc ; zero ) open import Ordinals module cardinal {n : Level } (O : Ordinals {n}) where open import logic -- import OD import OD hiding ( _⊆_ ) 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 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 _⊆_ : ( A B : HOD ) → Set n _⊆_ A B = {x : Ordinal } → odef A x → odef B x open _∧_ open _∨_ open Bool open _==_ open HOD record OrdBijection (A B : Ordinal ) : Set n where field fun← : (x : Ordinal ) → odef (* A) x → Ordinal fun→ : (x : Ordinal ) → odef (* B) x → Ordinal funB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( fun← x lt ) funA : (x : Ordinal ) → ( lt : odef (* B) x ) → odef (* A) ( fun→ x lt ) fiso← : (x : Ordinal ) → ( lt : odef (* B) x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x fiso→ : (x : Ordinal ) → ( lt : odef (* A) x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x ordbij-refl : { a b : Ordinal } → a ≡ b → OrdBijection a b ordbij-refl {a} refl = record { fun← = λ x _ → x ; fun→ = λ x _ → x ; funB = λ x lt → lt ; funA = λ x lt → lt ; fiso← = λ x lt → refl ; fiso→ = λ x lt → refl } open Injection open OrdBijection record IsImage (a b : Ordinal) (iab : Injection a b ) (x : Ordinal ) : Set n where field y : Ordinal ay : odef (* a) y x=fy : x ≡ i→ iab _ ay 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 im00 : {x : Ordinal } → IsImage a b iab x → x o< b im00 {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ ( λ j k → j o< k) (trans &iso (sym x=fy)) &iso (c<→o< (subst ( λ k → odef (* b) k) (sym &iso) (iB iab y ay)) ) record IsInverseImage (a b : Ordinal) (iab : Injection a b ) (x y : Ordinal ) : Set n where field ax : odef (* a) x x=fy : y ≡ i→ iab x ax InverseImage : {a : Ordinal} ( b : Ordinal ) → Injection a b → (y : Ordinal ) → HOD InverseImage {a} b iab y = record { od = record { def = λ x → IsInverseImage a b iab x y } ; odmax = & (* a) ; <odmax = im00 } where im00 : {x : Ordinal } → IsInverseImage a b iab x y → x o< & (* a) im00 {x} record { ax = ax ; x=fy = x=fy } = odef< ax Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image a iab ⊆ * b Image⊆b {a} {b} iab {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k) (sym x=fy) (iB iab y ay) _=c=_ : ( A B : HOD ) → Set n A =c= B = OrdBijection ( & A ) ( & B ) c=→≡ : {A B : HOD} → A =c= B → (A ≡ ?) ∧ (B ≡ ?) c=→≡ = ? ≡→c= : {A B : HOD} → A ≡ B → A =c= B ≡→c= = ? 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 open Data.Nat 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 : 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) } Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b Bernstein {a} {b} iab iba = be00 where be05 : {a b : Ordinal } → a o< b → Injection a b → Injection b a → ⊥ be05 {a} {b} a<b iab iba = TransFinite0 {λ x → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ } ind a b a<b iab iba where ind :(x : Ordinal) → ((y : Ordinal) → y o< x → (b : Ordinal) → y o< b → Injection y b → Injection b y → ⊥ ) → (b : Ordinal) → x o< b → Injection x b → Injection b x → ⊥ ind a prev b x<b (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject })= prev _ ? _ ? Uf fU where gf : Injection a a gf = record { i→ = λ x ax → fba (fab x ax) (b∋fab x ax) ; iB = λ x ax → a∋fba _ (b∋fab x ax) ; inject = λ x y ax ay eq → fab-inject _ _ ax ay ( fba-inject _ _ (b∋fab _ ax) (b∋fab _ ay) eq) } data gfImage : (i : ℕ) (x : Ordinal) → Set n where a-g : {x : Ordinal} → (ax : odef (* a) x ) → (¬ib : ¬ ( IsImage b a g x )) → gfImage 0 x next-gf : {x y : Ordinal} → {i : ℕ} → (gfiy : gfImage i y )→ (ix : IsImage a a gf x) → gfImage (suc i) x a∋gfImage : (i : ℕ) → {x : Ordinal } → gfImage i x → odef (* a) x a∋gfImage 0 {x} (a-g ax ¬ib) = ax a∋gfImage (suc i) {x} (next-gf lt record { y = y ; ay = ay ; x=fy = x=fy }) = subst (λ k → odef (* a) k ) (sym x=fy) (a∋fba _ (b∋fab y ay) ) C : ℕ → HOD -- Image {& (C i)} {a} (gf i) does not work C i = record { od = record { def = gfImage i } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage i lt) } record CN (x : Ordinal) : Set n where field i : ℕ gfix : gfImage i x UC : HOD UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt)) } b-UC : HOD b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt) } -- UC ⊆ * a -- f : UC → Image f UC is injection -- g : Image f UC → UC is injection UC⊆a : * (& UC) ⊆ * a UC⊆a {x} lt = a∋gfImage (CN.i be02) (CN.gfix be02) where be02 : CN x be02 = subst (λ k → odef k x) *iso lt b-UC⊆b : * (& b-UC) ⊆ * b b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt ) open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) fab-refl : {x : Ordinal } → {ax ax1 : odef (* a) x} → fab x ax ≡ fab x ax1 fab-refl {x} {ax} {ax1} = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) fba-refl : {x : Ordinal } → {bx bx1 : odef (* b) x} → fba x bx ≡ fba x bx1 fba-refl {x} {bx} {bx1} = cong (λ k → fba x k) ( HE.≅-to-≡ ( ∋-irr {* b} bx bx1 )) be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) be10 = record { i→ = be12 ; iB = be13 ; inject = ? } where be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal be12 x lt = i→ g x (proj1 be02) where be02 : odef (* b) x ∧ ( ¬ CN x ) be02 = subst (λ k → odef k x) *iso lt be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (be12 x lt) be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fba-refl } where be02 : odef (* b) x ∧ ( ¬ CN x ) be02 = subst (λ k → odef k x) *iso lt be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC) be11 = record { i→ = be13 ; iB = ? ; inject = ? } where be13 : (x : Ordinal) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x → Ordinal be13 x lt with subst (λ k → odef k x) *iso lt ... | record { y = y ; ay = ay ; x=fy = x=fy } = y where -- x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay)) be02 : odef (* b) y ∧ ( ¬ CN y ) be02 = subst (λ k → odef k y) *iso ay fUC = & (Image (& UC) {b} (Injection-⊆ UC⊆a f) ) -- C n → f (C n) fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a f) )) fU = record { i→ = be00 ; iB = λ x lt → be50 x lt ; inject = be51 } where be00 : (x : Ordinal) (lt : odef (* (& UC)) x) → Ordinal be00 x lt = be03 where be02 : CN x be02 = subst (λ k → odef k x) *iso lt be03 : Ordinal be03 with CN.i be02 | CN.gfix be02 ... | zero | a-g {x} ax ¬ib = fab x ax ... | suc i | next-gf {x} gfiy record { y = y ; ay = ay ; x=fy = x=fy } = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) )) be50 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f )))) (be00 x lt) be50 x lt1 = subst (λ k → odef k (be00 x lt1 )) (sym *iso) be03 where be02 : CN x be02 = subst (λ k → odef k x) *iso lt1 be03 : odef (Image (& UC) (Injection-⊆ UC⊆a f )) (be00 x lt1 ) be03 with CN.i be02 | CN.gfix be02 ... | zero | a-g {x} ax ¬ib = record { y = x ; ay = lt1 ; x=fy = fab-refl } ... | suc i | next-gf {x} gfiy record { y = y ; ay = ay ; x=fy = x=fy } = record { y = _ ; ay = lt1 ; x=fy = fab-refl } be51 : (x y : Ordinal) (ltx : odef (* (& UC)) x) (lty : odef (* (& UC)) y) → be00 x ltx ≡ be00 y lty → x ≡ y be51 x y ltx lty eq = be04 where be0x : CN x be0x = subst (λ k → odef k x) *iso ltx be0y : CN y be0y = subst (λ k → odef k y) *iso lty be04 : x ≡ y be04 with CN.i be0x | CN.gfix be0x | CN.i be0y | CN.gfix be0y ... | 0 | a-g ax ¬ib | 0 | a-g ax₁ ¬ib₁ = fab-inject _ _ ax ax₁ eq ... | 0 | a-g ax ¬ib | suc j | next-gf gfyi iy = fab-inject _ _ ax ay eq where ay : odef (* a) y ay = a∋gfImage (suc j) (next-gf gfyi iy ) ... | suc i | next-gf gfxi ix | 0 | a-g ay ¬ib = fab-inject _ _ ax ay eq where ax : odef (* a) x ax = a∋gfImage (suc i) (next-gf gfxi ix ) ... | suc i | next-gf gfxi ix | suc j | next-gf gfyi iy = fab-inject _ _ ax ay eq where ax : odef (* a) x ax = a∋gfImage (suc i) (next-gf gfxi ix ) ay : odef (* a) y ay = a∋gfImage (suc j) (next-gf gfyi iy ) Uf : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a f))) (& UC) Uf = record { i→ = ? ; iB = λ x lt → ? ; inject = ? } where be00 : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal be00 = ? be00 : OrdBijection a b be00 with trio< a b ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba ) ... | tri≈ ¬a b ¬c = ordbij-refl b ... | tri> ¬a ¬b c = ⊥-elim ( be05 c iba iab ) _c<_ : ( A B : HOD ) → Set n A c< B = ¬ ( Injection (& A) (& B) ) Card : OD Card = record { def = λ x → (a : Ordinal) → a o< x → ¬ OrdBijection a x } record Cardinal (a : Ordinal ) : Set (Level.suc n) where field card : Ordinal ciso : OrdBijection a card cmax : (x : Ordinal) → card o< x → ¬ OrdBijection a x Cardinal∈ : { s : HOD } → { t : Ordinal } → Ord t ∋ s → s c< Ord t Cardinal∈ = {!!} Cardinal⊆ : { s t : HOD } → s ⊆ t → ( s c< t ) ∨ ( s =c= t ) Cardinal⊆ = {!!} Cantor1 : { u : HOD } → u c< Power u Cantor1 = {!!} Cantor2 : { u : HOD } → ¬ ( u =c= Power u ) Cantor2 = {!!}