Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1414:180caeb6927b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 30 Jun 2023 18:10:40 +0900 |
| parents | c66ee9d43c05 |
| children | 85842347e270 |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 34 insertions(+), 32 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Fri Jun 30 16:37:32 2023 +0900 +++ b/src/cardinal.agda Fri Jun 30 18:10:40 2023 +0900 @@ -124,10 +124,10 @@ 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 = be70 - ; funA = be71 + fun← = λ x lt → ? + ; fun→ = λ x lt → ? + ; funB = ? + ; funA = ? ; fiso← = ? ; fiso→ = ? } where @@ -296,46 +296,48 @@ ... | a-g ax ¬ib = sym x=fy ... | next-gf t ix = sym x=fy - h : {x : Ordinal } → (ax : odef (* a) x) → Ordinal - h {x} ax with ODC.p∨¬p O (gfImage x) - ... | case1 cn = fU x (subst (λ k → odef k x ) (sym *iso) cn ) - ... | case2 ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ) + h : {x : Ordinal } → (ax : odef (* a) x) → gfImage x ∨ (¬ gfImage x) → Ordinal + h {x} ax (case1 cn) = fU x (subst (λ k → odef k x ) (sym *iso) cn ) + h {x} ax (case2 ncn) = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ) - h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → Ordinal - h⁻¹ {x} bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) - ... | case1 cn = Uf x (subst (λ k → odef k x) (sym *iso) cn) -- x ≡ f y - ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where -- ¬ x ≡ f y + h⁻¹ : {x : Ordinal } → (bx : odef (* b) x) → (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) ∨ ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) + → Ordinal + h⁻¹ {x} bx ( case1 cn) = Uf x (subst (λ k → odef k x) (sym *iso) cn) -- x ≡ f y + h⁻¹ {x} bx ( case2 ncn) = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where -- ¬ x ≡ f y be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫ - be70 : (x : Ordinal) (lt : odef (* a) x) → odef (* b) (h lt) - be70 x ax = ? - -- with ODC.p∨¬p O ( gfImage x ) - --... | 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 gfImage.i (subst (λ k → odef k x) *iso cn) | gfImage.gfix (subst (λ k → odef k x) *iso cn ) - -- ... | zero | a-g ax ¬ib = b∋fab x ax - -- ... | suc i | 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))) - --... | case2 ncn = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ))) + 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 ⟫ ))) - be71 : (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx) - be71 x bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) - ... | case1 cn = be03 (subst (λ k → odef k x) (sym *iso) cn) where + 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 or ) + 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 - ... | case2 ncn = proj1 (subst₂ (λ j k → odef j k ) *iso refl (iB be11 x (subst (λ k → odef k x) (sym *iso) be60) )) where + 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) )) where be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) ncn ⟫ - be72 : (x : Ordinal) (bx : odef (* b) x) → h (be71 x bx) ≡ x + be71-1 : (x : Ordinal) (bx : odef (* b) x) + → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) + → gfImage (h⁻¹ bx (case1 or) ) + 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 = ? + + be72 : (x : Ordinal) (bx : odef (* b) x) → h (be71 x bx ?) ? ≡ x be72 x bx with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) - be72 x bx | case1 img = ? where - be73 : gfImage (Uf x (subst (λ k → odef k x) (sym *iso) img )) - be73 = ? - be74 : Uf x (subst (λ k → odef k x) (sym *iso) img ) ≡ IsImage.y (subst (λ k → odef k x) *iso (subst (λ k → odef k x) (sym *iso) img)) - be74 = refl + be72 x bx | case1 record { y = y ; ay = ay ; x=fy = x=fy } = ? be72 x bx | case2 nimg = ?