Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1431:052f0fca7799
again... gfImage is not strictly positive, because it occurs
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Jul 2023 00:59:14 +0900 |
| parents | f2125be6fec1 |
| children | 8da1d318033b |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 78 insertions(+), 66 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Sat Jul 01 19:37:54 2023 +0900 +++ b/src/cardinal.agda Sun Jul 02 00:59:14 2023 +0900 @@ -76,6 +76,12 @@ im00 {x} record { y = y ; ay = ay ; x=fy = x=fy } = subst₂ ( λ j k → j o< k) (trans &iso (sym x=fy)) &iso (c<→o< (subst ( λ k → odef (* b) k) (sym &iso) (iB iab y ay)) ) +record IsImage0 (a b : HOD) (f : (x : Ordinal) → odef a x → Ordinal) (x : Ordinal ) : Set n where + field + y : Ordinal + ay : odef a y + x=fy : x ≡ f y ay + record IsInverseImage (a b : Ordinal) (iab : Injection a b ) (x y : Ordinal ) : Set n where field ax : odef (* a) x @@ -124,12 +130,12 @@ Bernstein : {a b : Ordinal } → Injection a b → Injection b a → OrdBijection a b Bernstein {a} {b} (f @ record { i→ = fab ; iB = b∋fab ; inject = fab-inject }) ( g @ record { i→ = fba ; iB = a∋fba ; inject = fba-inject }) = record { - fun← = λ x lt → h lt ? - ; fun→ = λ x lt → h⁻¹ lt ? - ; funB = be74 - ; funA = be75 - ; fiso← = λ x lt → be72 x lt (cc11 (a∋fba x lt) (cc20 lt)) - ; fiso→ = λ x lt → be73 x lt (cc10 (b∋fab x lt) (cc21 lt)) + fun← = λ x lt → h lt (cc0 x) + ; fun→ = λ x lt → h⁻¹ lt (cc1 x) + ; funB = λ x lt → be74 x lt (cc0 x) + ; funA = λ x lt → be75 x lt (cc1 x) + ; fiso← = λ x lt → be72 x lt (cc1 x) + ; fiso→ = λ x lt → be73 x lt (cc0 x) } where gf : Injection a a @@ -209,17 +215,20 @@ be16 {x} lt with subst (λ k → odef k x) *iso lt ... | ⟪ ax , ncn ⟫ = nimg ax ncn - nimg1 : {x : Ordinal} (ax : odef (* a) x) → (ncn : ¬ gfImage x) → IsImage b a g x - nimg1 {x} ax ncn = nimg ax ncn + FA : (x : Ordinal) → (ax : gfImage x) → Ordinal + FA x ax = fab x (a∋gfImage ax) - cc11-case2 : {x : Ordinal} (ax : odef (* a) x) → (ncn : ¬ gfImage x) - → ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ ax (nimg ax ncn)) - cc11-case2 {x} ax ncn record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → gfImage k) be113 (UC∋gf ay) ) where - be113 : fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡ x - be113 = begin - fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡⟨ fba-eq (sym x=fy) ⟩ - fba (g⁻¹ ax (nimg ax ncn) ) (b∋g⁻¹ ax (nimg ax ncn) ) ≡⟨ g⁻¹-iso ax (nimg ax ncn) ⟩ - x ∎ where open ≡-Reasoning + cc11-case2 : {x : Ordinal} (ax : odef (* a) x) + → (ncn : ¬ gfImage x) + → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax)) (g⁻¹ ax (nimg ax ncn)) + cc11-case2 {x} ax ncn record { y = y ; ay = ay ; x=fy = x=fy } with nimg ax ncn + ... | record { y = y1 ; ay = ay1 ; x=fy = x=fy1 } = ncn ( subst (λ k → gfImage k) be113 + (next-gf record { y = y ; ay = (a∋gfImage ay) ; x=fy = refl } ay ) ) where + be113 : fba (fab y (a∋gfImage ay)) (b∋fab y (a∋gfImage ay)) ≡ x + be113 = begin + fba (fab y (a∋gfImage ay)) (b∋fab y (a∋gfImage ay)) ≡⟨ fba-eq (sym x=fy) ⟩ + fba y1 ay1 ≡⟨ sym (x=fy1) ⟩ + x ∎ where open ≡-Reasoning be10 : Injection (& a-UC) (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) ) -- g⁻¹ x be10 = record { i→ = λ x lt → g⁻¹ (be15 lt) (be16 lt) ; iB = be17 ; inject = be18 } where @@ -248,9 +257,11 @@ be60 {b} {x} bx ncn = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫ cc10-case2 : {x : Ordinal } → (bx : odef (* b) x ) - → (x₁ : ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x ) - → ¬ gfImage (be13 x (subst (λ k → odef k x) (sym *iso) (be60 bx x₁))) - cc10-case2 = ? + → ¬ IsImage0 UC (* b) (λ x ax → fab x (a∋gfImage ax)) x + → ¬ gfImage (fba x bx) + cc10-case2 {x} bx nix (a-g ax ¬ib) = ¬ib record { y = _ ; ay = bx ; x=fy = refl } + cc10-case2 {x} bx nix (next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfy) + = nix record { y = _ ; ay = gfy ; x=fy = inject g _ _ bx (b∋fab y (a∋gfImage gfy)) (trans x=fy (fba-eq (fab-eq refl))) } be11 : Injection (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC) -- g x be11 = record { i→ = be13 ; iB = be14 ; inject = ? } where @@ -293,11 +304,20 @@ ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy = fab x (subst (λ k → odef (* a) k) (sym x=fy) (a∋fba _ (b∋fab y ay) )) + fU1 : (x : Ordinal) → odef UC x → Ordinal + fU1 x gfx = fab x (a∋gfImage gfx) + -- f (C n) → g (f (C n) ) ≡ C (suc i) 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 + b∋Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → odef (* b) x + b∋Uf1 x record { y = y ; ay = ay ; x=fy = x=fy } = subst (λ k → odef (* b) k ) (sym x=fy) (b∋fab y (a∋gfImage ay)) + + Uf1 : (x : Ordinal) → IsImage0 UC (* b) FA x → Ordinal + Uf1 x lt = fba x (b∋Uf1 x lt) + 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 : gfImage x @@ -338,23 +358,23 @@ → (ux : odef (* (& UC)) (Uf x cx)) → fU ( Uf x cx ) ux ≡ x UC-iso11 x cx ux = subst (λ k → fU (Uf x cx) k ≡ x) ( HE.≅-to-≡ ( ∋-irr {* (& UC)} {_} (be08 cx) ux)) (UC-iso1 x cx) - CC0 : (x : Ordinal) → (bx : odef (* a) x) → Set n - CC0 x ax = gfImage x ∨ (¬ gfImage x) + CC0 : (x : Ordinal) → Set n + CC0 x = gfImage x ∨ (¬ gfImage x) - CC1 : (x : Ordinal) → (bx : odef (* b) x) → Set n - CC1 x bx = gfImage (fba x bx) ∨ (¬ gfImage (fba x bx) ) + CC1 : (x : Ordinal) → Set n + CC1 x = IsImage0 UC (* b) FA x ∨ (¬ IsImage0 UC (* b) FA x) - cc0 : (x : Ordinal) → CC0 x ? + cc0 : (x : Ordinal) → CC0 x cc0 x = ODC.p∨¬p O (gfImage x) - cc1 : (x : Ordinal) → (bx : odef (* b) x) → CC1 x ? - cc1 x bx = ODC.p∨¬p O (gfImage (fba x bx) ) + cc1 : (x : Ordinal) → CC1 x + cc1 x = ODC.p∨¬p O (IsImage0 UC (* b) FA x) - cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt ) ? - cc20 = ? + cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt ) + cc20 {x} lt = cc0 (fba x lt) - cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) ? - cc21 = ? + cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) + cc21 {x} lt = cc1 (fab x lt) -- -- h : * a → * b @@ -368,55 +388,44 @@ -- -- otherwise not strict positive on gfImage error will happen - h : {x : Ordinal } → (ax : odef (* a) x) → CC0 x ax → Ordinal - h {x} ax (case1 cn) = fU x (subst (λ k → odef k x ) (sym *iso) cn ) + h : {x : Ordinal } → (ax : odef (* a) x) → CC0 x → Ordinal + h {x} ax (case1 cn) = fU1 x cn h {x} ax (case2 ncn) = g⁻¹ ax (nimg ax ncn) - h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → CC1 x bx → Ordinal - h⁻¹ {x} bx ( case1 cn) = Uf x ? -- x ≡ f y + h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → CC1 x → Ordinal + h⁻¹ {x} bx ( case1 cn) = Uf1 x cn -- x ≡ f y h⁻¹ {x} bx ( case2 ncn) = fba x bx - cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x bx) → CC0 (h⁻¹ bx cc1 ) ? - cc10 {x} bx (case1 x₁) = case1 ? -- (subst₂ (λ j k → odef j k ) *iso refl (be08 (subst (λ k → odef k x) (sym *iso) x₁))) - cc10 {x} bx (case2 x₁) = case2 ? -- (cc10-case2 bx ? ) - - cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x ax) → CC1 (h ax cc0 ) ? - cc11 {x} ax (case1 x₁) = case1 ? -- (subst₂ (λ j k → odef j k ) *iso refl (be04 (subst (λ k → odef k x) (sym *iso) x₁))) - cc11 {x} ax (case2 x₁) = case2 ? -- (cc11-case2 ax x₁) + cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x ) → CC0 (h⁻¹ bx cc1 ) + cc10 {x} bx (case1 record { y = y ; ay = ay ; x=fy = x=fy }) = + case1 (next-gf record { y = _ ; ay = a∋gfImage ay ; x=fy = fba-eq x=fy } ay ) + cc10 {x} bx (case2 x₁) = case2 (cc10-case2 bx x₁ ) - be70 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef (* b) (h lt or ) - be70 x ax ( case1 cn ) = be03 (subst (λ k → odef k x) (sym *iso) cn) where -- make the same condition for Uf - be03 : (cn : odef (* (& UC)) x) → odef (* b) (fU x cn ) - be03 cn with subst (λ k → odef k x) *iso cn - ... | a-g ax ¬ib = b∋fab x ax - ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } gfiy = b∋fab x - (subst (odef (* a)) (sym x=fy) (a∋fba (fab y ay) (b∋fab y ay))) - be70 x ax ( case2 ncn ) = ? -- proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ))) + cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x ) → CC1 (h ax cc0 ) + cc11 {x} ax (case1 x₁) = case1 record {y = _ ; ay = x₁ ; x=fy = refl } + cc11 {x} ax (case2 x₁) = case2 (cc11-case2 ax x₁) - be71 : (x : Ordinal) (bx : odef (* b) x) - → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) ∨ ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) )) - → odef (* a) (h⁻¹ bx ? ) - be71 x bx ( case1 cn ) = be03 (subst (λ k → odef k x) (sym *iso) cn) where - be03 : (cn : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) → odef (* a) (Uf x cn ) - be03 cn with subst (λ k → odef k x ) *iso cn - ... | record { y = y ; ay = ay ; x=fy = x=fy } = UC⊆a ay - be71 x bx ( case2 ncn ) = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) (be60 bx ncn)) )) + be70 : (x : Ordinal) (lt : odef (* a) x) → (or : CC0 x ) → odef (* b) (h lt or ) + be70 x ax ( case1 cn ) = b∋fab x (a∋gfImage cn) + be70 x ax ( case2 ncn ) = b∋g⁻¹ ax (nimg ax ncn) + + be71 : (x : Ordinal) (bx : odef (* b) x) → (or : CC1 x) → odef (* a) (h⁻¹ bx or ) + be71 x bx ( case1 cn ) = subst (λ k → odef (* a) k) (fba-eq refl) (a∋fba x bx ) + be71 x bx ( case2 ncn ) = a∋fba x bx be71-1 : (x : Ordinal) (bx : odef (* b) x) → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) → gfImage (h⁻¹ bx (case1 ? ) ) - be71-1 x bx cn = subst₂ (λ j k → odef j k ) *iso refl (be08 (subst (λ k → odef k x) (sym *iso) cn)) + be71-1 x bx cn = ? -- subst₂ (λ j k → odef j k ) *iso refl (be08 (subst (λ k → odef k x) (sym *iso) cn)) be70-1 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef ( Image (& UC) (Injection-⊆ UC⊆a f)) (h lt or ) be70-1 = ? - be74 : (x : Ordinal) (ax : odef (* a) x) → odef (* b) (h ax (cc0 x)) - be74 x ax with cc0 x - ... | case1 lt1 = ? - ... | case2 lt1 with iB be10 ? ? + be74 : (x : Ordinal) (ax : odef (* a) x) (cc0 : CC0 x) → odef (* b) (h ax cc0 ) + be74 x ax with cc0 ... | t = ? - be75 : (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx ? ) + be75 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x) → odef (* a) (h⁻¹ bx cc1 ) be75 x lt = ? fba-image : {x : Ordinal } → (bx : odef (* b) x) → odef (Image b g) (fba x bx) @@ -425,12 +434,15 @@ ImageUnique : {a b x : Ordinal } → {F : Injection a b} → (i j : odef (Image a F) x ) → IsImage.y i ≡ IsImage.y j ImageUnique {a} {b} {x} {F} i j = inject F _ _ (IsImage.ay i) (IsImage.ay j) (trans (sym (IsImage.x=fy i)) (IsImage.x=fy j)) - be72 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x bx) → h (be71 x bx ? ) (cc10 bx ? ) ≡ x - be72 x bx = ? + be72 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x ) → h (be75 x bx cc1) (cc0 (h⁻¹ bx cc1)) ≡ x + be72 x bx (case1 x₁) with cc0 (Uf1 x x₁) + ... | t = ? + be72 x bx (case2 x₁) = ? - be73 : (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ax ) → h⁻¹ (be70 x ax cc0) ? ≡ x + be73 : (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) → h⁻¹ (be74 x ax cc0) (cc1 (h ax cc0)) ≡ x be73 x ax (case1 x₁) = ? + be73 x ax (case2 x₁) = ? _c<_ : ( A B : HOD ) → Set n