Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1403:5476e93726e3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Jun 2023 10:01:29 +0900 |
| parents | d9eb3ae5fbad |
| children | 6dc3eb544387 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 40 insertions(+), 37 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Thu Jun 29 07:08:32 2023 +0900 +++ b/src/cardinal.agda Thu Jun 29 10:01:29 2023 +0900 @@ -155,7 +155,7 @@ UC = record { od = record { def = λ x → CN x } ; odmax = & (* a) ; <odmax = λ lt → odef< (a∋gfImage (CN.i lt) (CN.gfix lt)) } b-UC : HOD - b-UC = record { od = record { def = λ x → odef (* b) x ∧ (¬ CN x) } ; odmax = & (* b) ; <odmax = λ lt → odef< (proj1 lt) } + b-UC = record { od = record { def = λ x → (bx : odef (* b) x) → ¬ CN (fba x bx) } ; odmax = & (* b) ; <odmax = λ lt → ? } -- odef< (proj1 lt) } -- UC ⊆ * a -- f : UC → Image f UC is injection @@ -167,7 +167,7 @@ be02 = subst (λ k → odef k x) *iso lt b-UC⊆b : * (& b-UC) ⊆ * b - b-UC⊆b {x} lt = proj1 ( subst (λ k → odef k x) *iso lt ) + b-UC⊆b {x} lt = ? open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) @@ -180,15 +180,15 @@ be10 : Injection (& b-UC) (& (Image (& b-UC) {a} (Injection-⊆ b-UC⊆b g) )) 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 ) - be02 = subst (λ k → odef k x) *iso lt + be12 x lt = i→ g x ? where + be02 : odef (* b) x → ( ¬ CN x ) + be02 = ? be13 : (x : Ordinal) (lt : odef (* (& b-UC)) x) → odef (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (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) be02 ; x=fy = fba-eq refl } where - be02 : odef (* b) x ∧ ( ¬ CN x ) - be02 = subst (λ k → odef k x) *iso lt + be13 x lt = subst (λ k → odef k ?) (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 (* (& 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 + 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 = be14 ; inject = be15 } where @@ -207,11 +207,11 @@ 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 + ... | record { y = y ; ay = ay ; x=fy = x=fy } = inject g _ _ ? ? (sym x=fy) where be02 : odef (* b) x ∧ ( ¬ CN x ) - be02 = subst (λ k → odef k x) *iso cx + be02 = ? be03 : odef (* b) y ∧ ( ¬ CN y ) - be03 = subst (λ k → odef k y) *iso ay + be03 = ? 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 @@ -299,33 +299,36 @@ be24 = inject g _ _ bx (b∋fab y ay) x=fy be25 : odef UC y be25 = record { i = i ; gfix = t } - be20 | case2 ⟪ agx , ncn ⟫ = case2 (subst (λ k → odef k (fba x bx) ) (sym *iso) be21 ) where - be21 : odef (Image (& b-UC) (Injection-⊆ b-UC⊆b g)) (fba x bx) - be21 = record { y = g⁻¹ agx be22 - ; ay = subst (λ k → odef k (g⁻¹ agx be22)) (sym *iso) ⟪ b∋g⁻¹ agx be22 , be23 ⟫ ; x=fy = ? } where - be22 : ¬ odef (C 0) (fba x bx) - be22 = λ nc0 → ncn record { i = 0 ; gfix = nc0 } + be20 | case2 ⟪ agx , ncn ⟫ = 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 (* (& (Image (& b-UC) (Injection-⊆ b-UC⊆b g)))) (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 - be25 : ¬ CN (g⁻¹ agx be22) - be25 cn = be26 (CN.i cn) _ ? (CN.gfix cn) ? where - be26 : (i : ℕ) (y : Ordinal) (ay : odef (* a) y) ( gfi : gfImage i y ) → ¬ CN y → ⊥ - be26 0 y ay (a-g ax ¬ib) ncy = ⊥-elim ( ncy record { i = 0 ; gfix = a-g ax ¬ib } ) - be26 (suc i) y ay (next-gf record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } gfi) ncy = be26 i y1 ay1 gfi be27 where - be27 : ¬ (CN y1) - be27 cn with CN.i cn | CN.gfix cn - ... | 0 | t @ (a-g ax ¬ib) = ncy record { i = suc 0 - ; gfix = next-gf record { y = y1 ; ay = ax ; x=fy = trans x=fy1 (fba-eq (fab-eq refl)) } t } - ... | suc i | t @ (next-gf ix t1) = ncy record { i = suc (suc i) - ; gfix = next-gf record { y = y1 ; ay = a∋gfImage _ t ; x=fy = trans x=fy1 (fba-eq (fab-eq refl)) } t } - be23 : ¬ CN (g⁻¹ agx be22) -- g⁻¹ (g x ) -- ¬ CN x - be23 cng with CN.i cng | CN.gfix cng - ... | 0 | a-g ax ¬ib = ⊥-elim ( ¬ib record { y = ? ; ay = ? ; x=fy = ? } ) - ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ⊥-elim (ncn record { i = suc i ; gfix = ? }) - be24 : ¬ CN x - be24 cng with CN.i cng | CN.gfix cng - ... | 0 | a-g ax ¬ib = ⊥-elim ( ¬ib record { y = g⁻¹ agx be22 ; ay = ? ; x=fy = ? } ) - ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t = ⊥-elim (ncn record { i = suc i ; gfix = ? }) + 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 : IsImage (& b-UC) _ (Injection-⊆ b-UC⊆b g) (fba x bx) + be32 = record { y = x ; ay = ? ; x=fy = fba-eq refl } + + h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal + h {x} ax with ODC.p∨¬p O ( CN x ) + ... | case1 cn = fU x (subst (λ k → odef k x ) (sym *iso) cn) + ... | case2 ncn = i→ be10 (g⁻¹ ax ?) (subst (λ k → odef k (g⁻¹ ax ?) ) (sym *iso) (λ bx cngx → ? ) ) + + h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → Ordinal + h⁻¹ {x} bx with ODC.p∨¬p O ( CN (fba x bx) ) + ... | case1 cn = fU (fba x bx) (subst (λ k → odef k (fba x bx) ) (sym *iso) cn ) + ... | case2 ncn = i→ be11 (g⁻¹ (a∋fba x bx) ?) (subst (λ k → odef k (g⁻¹ (a∋fba x bx) ?)) (sym *iso) + record { y = x ; ay = subst (λ k → odef k x) (sym *iso) (λ bx cngx → ?) ; x=fy = ? } ) _c<_ : ( A B : HOD ) → Set n A c< B = ¬ ( Injection (& A) (& B) )