Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1392:8645a167d76b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 26 Jun 2023 15:52:14 +0900 |
| parents | 250e52f15f43 |
| children | c67ecdf89e77 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 66 insertions(+), 93 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Mon Jun 26 10:42:16 2023 +0900 +++ b/src/cardinal.agda Mon Jun 26 15:52:14 2023 +0900 @@ -116,94 +116,6 @@ 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 } -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 - - 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)) } - - -- 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 - - fU : Injection (& UC) (& (Image (& UC) {b} (Injection-⊆ UC⊆a f) )) - fU = record { i→ = λ x lt → IsImage.y (be10 x lt) ; iB = λ x lt → be20 (IsImage.y (be10 x lt)) (be21 x lt) ; inject = ? } where - be10 : (x : Ordinal) (lt : odef (* (& UC)) x) → IsImage _ _ (Injection-⊆ UC⊆a f) x - be20 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x - be20 x lt = subst ( λ k → odef k x ) (sym *iso) (be10 x lt ) - be21 : (x : Ordinal) (lt : odef (* (& UC)) x) → odef (* (& UC)) (IsImage.y (be10 x lt)) - be21 = ? - g⁻¹ : ( x : Ordinal) → odef (* b) x → Ordinal - g⁻¹ x bx = fba _ bx - a∋g⁻¹ : ( x : Ordinal) → (bx : odef (* b) x ) → odef (* a) (g⁻¹ x bx ) - a∋g⁻¹ x bx = a∋fba x bx - is-g⁻¹ : { x : Ordinal} → (bx : odef (* b) x ) → g⁻¹ (fba x ?) ? ≡ x - is-g⁻¹ {x} bx = begin - ? ≡⟨ ? ⟩ - ? ∎ where - open ≡-Reasoning - be10 x lt = record { y = be14 _ (CN.gfix be02) ; ay = ? ; x=fy = ? } where - be02 : CN x - be02 = subst (λ k → odef k x) *iso lt - be14 : (i : ℕ) → {x : Ordinal } → gfImage i x → Ordinal - be05 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → odef (* a) (be14 i gfi ) - be14 0 {x} (a-g ax ¬ib) = x - be14 (suc i) {x} (next-gf lt _) = fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) - be05 0 {x} (a-g ax ¬ib) = ax - be05 (suc i) {x} (next-gf lt _) = a∋fba ( fab (be14 i lt) (be05 i lt) ) ( b∋fab _ (be05 i lt)) - be16 : (i : ℕ) → {x : Ordinal } → (gfi : gfImage i x) → IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 i gfi) - be16 0 {x} (a-g ax ¬ib) = record { y = ? - ; ay = subst (λ k → odef k ? ) (sym *iso) record { i = 0 ; gfix = a-g ? ?} ; x=fy = ? } - be16 (suc i) {x} (next-gf ix ix₁) = record { y = ? ; ay = ? ; x=fy = ? } - be11 : IsImage _ _ ((Injection-⊆ UC⊆a f)) (be14 _ (CN.gfix be02)) - be11 = be16 _ (CN.gfix be02) - - gU : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a f))) (& UC) - gU = ? - - -- 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 @@ -213,11 +125,72 @@ 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 = ? + 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)) } + + -- 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 + + 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 )) + + 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 = ? } 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 } + + Uf : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a f))) (& UC) + Uf = ? + be00 : OrdBijection a b be00 with trio< a b ... | tri< a ¬b ¬c = ⊥-elim ( be05 a iab iba )