Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1398:d586aaa9b0bd
one Uf iso done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 28 Jun 2023 08:27:49 +0900 |
| parents | 94baa4bdfd7d |
| children | 59346935f8a4 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 70 insertions(+), 66 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Wed Jun 28 07:34:01 2023 +0900 +++ b/src/cardinal.agda Wed Jun 28 08:27:49 2023 +0900 @@ -227,7 +227,7 @@ 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 + 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 @@ -235,85 +235,89 @@ 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 } + ... | 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) )) - 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 } + -- 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 } - 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 ) - + -- 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 ) + -- -- 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 + 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 } = 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))) + ... | 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))) UC-iso0 : (x : Ordinal ) → (cx : odef (* (& UC)) x ) → i→ Uf ( i→ fU x cx ) (iB fU x cx) ≡ x - UC-iso0 x cx = ? where + 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 - ... | record { y = y ; ay = ay ; x=fy = x=fy } = ? -- fba (fab x _) _ = x - be03 | suc i | next-gf s ix | cb with subst (λ k → odef k (fab x _) ) *iso cb - ... | record { y = y ; ay = ay ; x=fy = x=fy } = ? + ... | zero | a-g ax ¬ib | cb with subst (λ k → odef k _ ) *iso cb | inspect (i→ 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 + ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject f _ _ ax (UC⊆a ay) x=fy ) where + 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 = ? + -- 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