Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1405:6db21bb5e704
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Jun 2023 11:17:20 +0900 |
| parents | 6dc3eb544387 |
| children | ba377f7d0c40 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 52 insertions(+), 65 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Thu Jun 29 10:41:50 2023 +0900 +++ b/src/cardinal.agda Thu Jun 29 11:17:20 2023 +0900 @@ -178,25 +178,40 @@ 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 )) + g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → ¬ odef (C 0) x → Ordinal + g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x ) + ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = y + ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) ) + + b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x) → odef (* b) (g⁻¹ ax nc0) + b∋g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x ) + ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ay + ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) ) + + g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x ) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x + g⁻¹-iso {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x ) + ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy + ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) ) + be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) ) - be10 = record { i→ = be12 ; iB = ? ; inject = be14 } where - be12 : (x : Ordinal) → odef (* (& a-UC)) x → Ordinal - be12 x lt = i→ g x (proj1 ? ) where - be02 : odef (* b) x ∧ ( ¬ CN ? ) - be02 = ? - be13 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (& (Image (& a-UC) (Injection-⊆ a-UC⊆a ?)))) (be12 x lt) - be13 x lt = subst (λ k → odef k (be12 x lt)) (sym *iso) record { y = x ; ay = subst (λ k → odef k x) (sym *iso) ? ; x=fy = fba-eq refl } where - be02 : odef (* b) x ∧ ( ¬ CN x ) - be02 = ? - be14 : (x y : Ordinal) (ltx : odef (* (& a-UC)) x) (lty : odef (* (& a-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 + be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = ? } where + be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x + be15 = ? + be16 : {x : Ordinal } → odef (* (& a-UC)) x → ¬ odef (C 0) x + be16 = ? + be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt)) + be17 = ? be11 : Injection (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC) - be11 = record { i→ = ? ; iB = ? ; inject = ? } where - be13 : (x : Ordinal) → odef (* (& (Image (& a-UC) (Injection-⊆ a-UC⊆a ?)))) x → Ordinal - be13 x lt = ? - be14 : (x : Ordinal) (lt : odef (* (& (Image (& a-UC) ?))) x) → odef (* (& a-UC)) (be13 x lt) - be14 x lt = ? + be11 = record { i→ = be13 ; iB = be14 ; inject = ? } where + be13 : (x : Ordinal) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x → Ordinal + be13 x lt = fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) + be14 : (x : Ordinal) (lt : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* (& a-UC)) (be13 x lt) + be14 x lt = subst (λ k → odef k (be13 x lt)) (sym *iso) ⟪ a∋fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) , ? ⟫ where + be16 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) + be16 = proj2 ( subst (λ k → odef k x) (*iso) lt ) + be15 : ¬ CN (be13 x lt) + be15 = ? a-UC-iso0 : (x : Ordinal ) → (cx : odef (* (& a-UC)) x ) → i→ be11 ( i→ be10 x cx ) (iB be10 x cx) ≡ x a-UC-iso0 x cx = ? @@ -232,15 +247,15 @@ 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 : 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 record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } s | cb with + be02 : CN x + be02 = subst (λ k → odef k x) *iso 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 record { y = x1 ; ay = ax1 ; x=fy = x=fx1 } s | 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 + ... | 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) ) @@ -250,33 +265,19 @@ 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 - - g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → ¬ odef (C 0) x → Ordinal - g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x ) - ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = y - ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) ) + 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 - b∋g⁻¹ : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x) → odef (* b) (g⁻¹ ax nc0) - b∋g⁻¹ {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x ) - ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ay - ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) ) - - g⁻¹-iso : {x : Ordinal } → (ax : odef (* a) x) → (nc0 : ¬ odef (C 0) x ) → fba (g⁻¹ ax nc0) (b∋g⁻¹ ax nc0) ≡ x - g⁻¹-iso {x} ax nc0 with ODC.p∨¬p O ( IsImage b a g x ) - ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym x=fy - ... | case2 ¬ism = ⊥-elim ( nc0 ( a-g ax ¬ism ) ) - + -- be11 : Injection (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC) Img∨ : (x : Ordinal) → (bx : odef (* b) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x - ∨ odef (* (& (Image (& a-UC) ?))) (fba x bx) + ∨ odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x Img∨ x bx = be20 where - be20 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (& (Image (& a-UC) ?))) (fba x bx) - be20 with ∨L＼X {* a} {UC} (a∋fba x bx) - ... | case1 uc = case1 (subst (λ k → odef k x) (sym *iso) be21 ) where + be20 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x + be20 with ∨L＼X {* a} {UC} (a∋fba x bx) + ... | case1 uc = case1 (subst (λ k → odef k x) (sym *iso) be21 ) where be21 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) x be21 with CN.i uc | CN.gfix uc ... | 0 | a-g ax ¬ib = ⊥-elim (¬ib record { y = x ; ay = bx ; x=fy = refl } ) @@ -286,25 +287,11 @@ be24 = inject g _ _ bx (b∋fab y ay) x=fy be25 : odef UC y be25 = record { i = i ; gfix = t } - be20 | case2 ⟪ agx , ncn ⟫ = be21 where + be20 | case2 ⟪ agx , ncn ⟫ = case2 be21 where be22 : ¬ odef (C 0) (fba x bx) -- condition for g⁻¹ be22 = λ nc0 → ncn record { i = 0 ; gfix = nc0 } - be21 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef ? (fba x bx) - be21 with ODC.p∨¬p O (IsImage (& UC) _ (Injection-⊆ UC⊆a f) x) -- p∨¬p (CN (g⁻¹ agx be22) ) causes recursive record - ... | case1 cn = case1 (subst (λ k → odef k x) (sym *iso) cn ) - ... | case2 ¬cn = case2 (subst (λ k → odef k (fba x bx)) (sym *iso) be32 ) where - be23 : x ≡ g⁻¹ agx be22 - be23 = inject g _ _ bx (b∋g⁻¹ agx be22) (sym (g⁻¹-iso agx be22 )) - be30 : CN (fba x bx) → ⊥ - be30 = ncn - be31 : ¬ IsImage (& UC) _ (Injection-⊆ UC⊆a f) x - be31 = ¬cn - be25 : ¬ CN x - be25 cn with CN.i cn | CN.gfix cn - ... | 0 | a-g ax ¬ib = ? - ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ? - be32 : ? - be32 = ? + be21 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x + be21 = ? h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal h {x} ax with ODC.p∨¬p O ( CN x )