Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1396:ac854f01352b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 27 Jun 2023 18:38:41 +0900 |
| parents | e39c2bffb86e |
| children | 94baa4bdfd7d |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 62 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Tue Jun 27 10:50:07 2023 +0900 +++ b/src/cardinal.agda Tue Jun 27 18:38:41 2023 +0900 @@ -178,8 +178,14 @@ 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 )) + fab-eq : {x y : Ordinal } → {ax : odef (* a) x} {ax1 : odef (* a) y} → x ≡ y → fab x ax ≡ fab y ax1 + fab-eq {x} {x} {ax} {ax1} refl = cong (λ k → fab x k) ( HE.≅-to-≡ ( ∋-irr {* a} ax ax1 )) + + fba-eq : {x y : Ordinal } → {bx : odef (* b) x} {bx1 : odef (* b) y} → x ≡ y → fba x bx ≡ fba y bx1 + fba-eq {x} {x} {bx} {bx1} refl = 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 + be10 = record { i→ = be12 ; iB = be13 ; inject = be14 } where be12 : (x : Ordinal) → odef (* (& b-UC)) x → Ordinal be12 x lt = i→ g x (proj1 be02) where be02 : odef (* b) x ∧ ( ¬ CN x ) @@ -188,15 +194,35 @@ 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 - + be14 : (x y : Ordinal) (ltx : odef (* (& b-UC)) x) (lty : odef (* (& b-UC)) y) → be12 x ltx ≡ be12 y lty → x ≡ y + be14 x y ltx lty eq = inject g _ _ (proj1 (subst (λ k → odef k x) *iso ltx)) (proj1 (subst (λ k → odef k y) *iso lty)) eq be11 : Injection (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) (& b-UC) - be11 = record { i→ = be13 ; iB = ? ; inject = ? } where + be11 = record { i→ = be13 ; iB = be14 ; inject = be15 } 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 + ... | record { y = y ; ay = ay ; x=fy = x=fy } = y -- g⁻¹ x=fy : x ≡ fba y (proj1 (subst (λ k → OD.def (od k) y) *iso ay)) + be14 : (x : Ordinal) (lt : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) → odef (* (& b-UC)) (be13 x lt) + be14 x lt with subst (λ k → odef k x) *iso lt + ... | record { y = y ; ay = ay ; x=fy = x=fy } = ay + be15 : (x y : Ordinal) (ltx : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) x) + (lty : odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) y) → + be13 x ltx ≡ be13 y lty → x ≡ y + be15 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 } + = trans x=fix (trans ( fba-eq eq ) (sym x=fiy ) ) + + b-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& b-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx) ≡ x + b-UC-iso0 x cx with subst (λ k → odef k ( i→ be10 x cx ) ) *iso (iB be10 x cx) + ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ (proj1 be03) (proj1 be02) (sym x=fy) where + be02 : odef (* b) x ∧ ( ¬ CN x ) + be02 = subst (λ k → odef k x) *iso cx + be03 : odef (* b) y ∧ ( ¬ CN y ) + be03 = subst (λ k → odef k y) *iso ay + + b-UC-iso1 : (x : Ordinal ) → (cx : odef (* (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g)))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx) ≡ x + 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) @@ -243,21 +269,44 @@ ay = a∋gfImage (suc j) (next-gf gfyi iy ) + -- 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 = be01 ; 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 } = 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 be02 where + 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 - be02 : CN (be00 x lt) - be02 = record { i = suc (CN.i be04 ) ; gfix = next-gf (CN.gfix be04) record { y = ? ; ay = ? ; x=fy = ? } } - be03 : x ≡ fab y (a∋gfImage (CN.i be04) (CN.gfix be04)) - be03 = x=fy - + 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))) + + UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x + UC-iso0 x cx = ? + + 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 = ? + be00 : OrdBijection a b be00 with trio< a b