Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/cardinal.agda @ 1387:003424a36fed
is this agda's bug?
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 25 Jun 2023 15:58:16 +0900 |
parents | 66a6804d867b |
children | 2e53a8e6fa5f |
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 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)) ) Image⊆b : { a b : Ordinal } → (iab : Injection a b) → Image 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 Bernstein1 : {a b : Ordinal } → a o< b → Injection a b ∧ Injection b a → Injection (b - a) b ∧ Injection b (b - a) Bernstein1 {a} {b} a<b ⟪ f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject } , g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject } ⟫ = ⟪ record { i→ = f0 ; iB = b∋f0 ; inject = f0-inject } , record { i→ = f1 ; iB = b∋f1 ; inject = f1-inject } ⟫ where C : ℕ → HOD gf : (i : ℕ) → Injection (& (C i)) a gf 0 = record { i→ = λ x cx → fba x ? ; iB = ? ; inject = ? } gf (suc i) = record { i→ = be00 ; iB = ? ; inject = ? } where be00 : (x : Ordinal) → odef (* (& (C (suc i)))) x → Ordinal be00 x lt with subst (λ k → odef k x) *iso lt | inspect C (suc i) ... | t | record { eq = eq1 } = ? C 0 = (* a) \ Image g C (suc i) = Image {& (C i)} {a} (gf i) record CN (x : Ordinal) : Set n where field i : ℕ cn=x : & (C i) ≡ x UC : HOD UC = record { od = record { def = λ x → CN x } ; odmax = a ; <odmax = ? } -- Injection (b - a) b f0 : (x : Ordinal) → odef (* (b - a)) x → Ordinal f0 x lt with subst (λ k → odef k x) *iso lt ... | ⟪ bx , ¬ax ⟫ = fab (fba x bx) (a∋fba x bx) b∋f0 : (x : Ordinal) (lt : odef (* (b - a)) x) → odef (* b) (f0 x lt) b∋f0 x lt with subst (λ k → odef k x) *iso lt ... | ⟪ bx , ¬ax ⟫ = b∋fab (fba x bx) (a∋fba x bx) f0-inject : (x y : Ordinal) (ltx : odef (* (b - a)) x) (lty : odef (* (b - a)) y) → f0 x ltx ≡ f0 y lty → x ≡ y f0-inject x y ltx lty eq = fba-inject _ _ (b-a⊆b ltx) (b-a⊆b lty) ( fab-inject _ _ (a∋fba x (b-a⊆b ltx)) (a∋fba y (b-a⊆b lty)) eq ) -- Injection b (b - a) f1 : (x : Ordinal) → odef (* b) x → Ordinal f1 x lt = ? b∋f1 : (x : Ordinal) (lt : odef (* b) x) → odef (* (b - a)) (f1 x lt) b∋f1 x lt = ? f1-inject : (x y : Ordinal) (ltx : odef (* b) x) (lty : odef (* b) y) → f1 x ltx ≡ f1 y lty → x ≡ y f1-inject x y ltx lty 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 x prev b x<b ixb ibx = prev _ be01 _ be02 (proj1 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) (proj2 (Bernstein1 x<b ⟪ ixb , ibx ⟫)) where be01 : (b - x) o< x be01 = ? be02 : (b - x) o< b be02 = ? 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 = {!!}