Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1399:59346935f8a4
iso in bernstein done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Jun 2023 08:56:28 +0900 |
| parents | d586aaa9b0bd |
| children | 1c7b0a040d9c |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 38 insertions(+), 81 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Wed Jun 28 08:27:49 2023 +0900 +++ b/src/cardinal.agda Wed Jun 28 08:56:28 2023 +0900 @@ -130,7 +130,7 @@ ((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 + ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-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) @@ -224,91 +224,39 @@ b-UC-iso1 x cx with subst (λ k → odef k x ) *iso cx ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy - 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 → ? ; 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 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) )) - -- e50 : (x : Ordinal) (lt : odef (* (& UC)) x) - -- → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f )))) (be00 x lt) - -- e50 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 } - - -- e51 : (x y : Ordinal) (ltx : odef (* (& UC)) x) (lty : odef (* (& UC)) y) → be00 x ltx ≡ be00 y lty → x ≡ y - -- e51 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 ) - -- + fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal + fU 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 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) )) -- f (C n) → g (f (C n) ) ≡ C (suc i) - Uf : Injection (& (Image (& UC) {b} (Injection-⊆ UC⊆a f))) (& UC) - Uf = record { i→ = be00 ; iB = ? ; inject = ? } where - be00 : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal - be00 x lt with subst (λ k → odef k x ) *iso lt - ... | record { y = y ; ay = ay ; x=fy = x=fy } = y - -- fba x (subst (λ k → odef (* b) k ) (trans fab-refl (sym x=fy)) (b∋fab y (UC⊆a ay) ) ) - -- be01 : (x : Ordinal) → (lt : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ) → odef (* (& UC)) (be00 x lt) - -- be01 x lt with subst (λ k → odef k x) *iso lt - -- ... | record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ (λ j k → odef j k ) (sym *iso) fba-refl - -- record { i = suc (CN.i be04 ) ; gfix = next-gf (CN.gfix be04) record { y = y ; ay = a∋gfImage (CN.i be04) (CN.gfix be04) ; x=fy = be06 } } - -- where - -- be04 : CN y - -- be04 = subst (λ k → odef k y) *iso ay - -- bx : odef (* b) x - -- bx = subst (λ k → odef (* b) k ) (sym x=fy) ( b∋fab y (a∋gfImage (CN.i be04) (CN.gfix be04))) - -- be06 : fba x bx ≡ fba (fab y (a∋gfImage (CN.i be04) (CN.gfix be04))) (b∋fab y (a∋gfImage (CN.i be04) (CN.gfix be04)) ) - -- be06 = fba-eq x=fy - -- be02 : (x y : Ordinal) (ltx : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a (record { i→ = fab ; iB = b∋fab ; inject = fab-inject }))))) x) - -- (lty : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a (record { i→ = fab ; iB = b∋fab ; inject = fab-inject }))))) y) → - -- be00 x ltx ≡ be00 y lty → x ≡ y - -- be02 x y ltx lty eq with subst (λ k → odef k x) *iso ltx | subst (λ k → odef k y) *iso lty - -- ... | record { y = ix ; ay = aix ; x=fy = x=fix } | record { y = iy ; ay = aiy ; x=fy = x=fiy } - -- = inject g _ _ bx by (trans fba-refl (trans eq fba-refl )) where - -- be04 : CN ix - -- be04 = subst (λ k → odef k ix) *iso aix - -- be06 : CN iy - -- be06 = subst (λ k → odef k iy) *iso aiy - -- bx : odef (* b) x - -- bx = subst (λ k → odef (* b) k ) (sym x=fix) ( b∋fab ix (a∋gfImage (CN.i be04) (CN.gfix be04))) - -- by : odef (* b) y - -- by = subst (λ k → odef (* b) k ) (sym x=fiy) ( b∋fab iy (a∋gfImage (CN.i be06) (CN.gfix be06))) + Uf : (x : Ordinal) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal + Uf x lt with subst (λ k → odef k x ) *iso lt + ... | record { y = y ; ay = ay ; x=fy = x=fy } = y - UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x + be04 : {x : Ordinal } → (cx : odef (* (& UC)) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) (fU x cx) + be04 {x} cx = subst (λ k → odef k (fU x cx) ) (sym *iso) be06 where + be02 : CN x + be02 = subst (λ k → odef k x) *iso cx + be06 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) (fU x cx) + be06 with CN.i be02 | CN.gfix be02 + ... | zero | a-g ax ¬ib = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-refl } + ... | suc i | next-gf gfiy record { y = y ; ay = ay ; x=fy = x=fy } + = record { y = x ; ay = subst (λ k → odef k x) (sym *iso) be02 ; x=fy = fab-refl } + + UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → Uf ( fU x cx ) (be04 cx) ≡ x UC-iso0 x cx = be03 where be02 : CN x be02 = subst (λ k → odef k x) *iso cx - be03 : i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x - be03 with CN.i be02 | CN.gfix be02 | iB fU x cx - ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect (i→ fU x) cx + be03 : Uf ( fU x cx ) (be04 cx) ≡ x + be03 with CN.i be02 | CN.gfix be02 | be04 cx + ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect (fU x) cx ... | record { y = y ; ay = ay ; x=fy = x=fy } | record { eq = refl } = sym ( inject f _ _ ax (UC⊆a ay) x=fy ) be03 | suc i | next-gf s record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } | cb with subst (λ k → odef k (fab x (subst (odef (* a)) (sym x=fx1) (a∋fba (fab x1 ax1) (b∋fab x1 ax1)))) ) *iso cb @@ -316,8 +264,17 @@ ax : odef (* a) x ax = subst (λ k → odef (* a) k ) (sym x=fx1) ( a∋fba _ (b∋fab x1 ax1) ) - -- UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) → i→ fU ( i→ Uf x cx ) (iB Uf x cx) ≡ x - -- UC-iso1 = ? + be08 : {x : Ordinal } → (cx : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* (& UC)) (Uf x cx) + be08 {x} cx with subst (λ k → odef k x) *iso cx + ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay + + UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& UC) {b} (Injection-⊆ UC⊆a f)))) x ) → fU ( Uf x cx ) (be08 cx) ≡ x + UC-iso1 x cx = be14 where + be14 : fU ( Uf x cx ) (be08 cx) ≡ x + be14 with subst (λ k → odef k x) *iso cx + ... | record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → OD.def (od k) y) *iso ay) | CN.gfix (subst (λ k → OD.def (od k) y) *iso ay) + ... | 0 | a-g ax ¬ib = sym x=fy + ... | (suc i) | next-gf t ix = sym x=fy be00 : OrdBijection a b