# HG changeset patch # User Shinji KONO # Date 1688090286 -32400 # Node ID 1e2c77c1227d1b6cd4f71872afd22abbbe1d41eb # Parent 2fe6908fb48e3755e437170ddef7061d96d550a4 ... diff -r 2fe6908fb48e -r 1e2c77c1227d src/cardinal.agda --- a/src/cardinal.agda Fri Jun 30 06:11:05 2023 +0900 +++ b/src/cardinal.agda Fri Jun 30 10:58:06 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← = ? - ; fun→ = ? - ; funB = ? - ; funA = ? + fun← = λ x lt → h lt + ; fun→ = λ x lt → h⁻¹ lt + ; funB = be70 + ; funA = be71 ; fiso← = ? ; fiso→ = ? } where @@ -178,6 +178,11 @@ 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 )) + UC∋gf : {y : Ordinal } → (uy : odef (* (& UC)) y ) → CN ( fba (fab y (UC⊆a uy) ) (b∋fab y (UC⊆a uy))) + UC∋gf {y} uy = record { i = suc (CN.i uc00) ; gfix = next-gf record { y = _ ; ay = UC⊆a uy ; x=fy = fba-eq (fab-eq refl) } (CN.gfix uc00) } where + uc00 : CN y + uc00 = subst (λ k → odef k y) *iso uy + 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 @@ -193,7 +198,10 @@ ... | 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) )) ) + g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : ¬ odef (C 0) (fba x bx) ) → g⁻¹ (a∋fba x bx) nc0 ≡ x + g⁻¹-iso1 {x} bx nc0 = inject g _ _ (b∋g⁻¹ (a∋fba x bx) nc0) bx (g⁻¹-iso (a∋fba x bx) nc0) + + 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 be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x be15 {x} lt with subst (λ k → odef k x) *iso lt @@ -202,30 +210,47 @@ be16 {x} lt nc0 with subst (λ k → odef k x) *iso lt ... | ⟪ ax , ncn ⟫ = ⊥-elim ( ncn record { i = 0 ; gfix = nc0 } ) be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt)) - be17 x lt with subst (λ k → odef k x) *iso lt - ... | ⟪ ax , ncn ⟫ = subst₂ ( λ j k → odef j k ) (sym *iso) ? ⟪ b∋g⁻¹ (be15 lt) (be16 lt), ? ⟫ - be18 : ¬ odef (* (& (Image (& UC) (Injection-⊆ (λ {x} lt → a∋gfImage (CN.i (subst (λ k → odef k x) *iso lt)) (CN.gfix (subst (λ k → odef k x) *iso lt))) f)))) (g⁻¹ (be15 lt) (be16 lt)) - be18 = ? - + be17 x lt = subst ( λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) (sym *iso) ⟪ be19 , + (λ img → be18 be14 (subst (λ k → odef k (g⁻¹ (be15 lt) (be16 lt))) *iso img) ) ⟫ where + be14 : odef a-UC x + be14 = subst (λ k → odef k x) *iso lt + be19 : odef (* b) (g⁻¹ (be15 lt) (be16 lt)) + be19 = b∋g⁻¹ (be15 lt) (be16 lt) + be18 : odef a-UC x → ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ (be15 lt) (be16 lt)) + be18 ⟪ ax , ncn ⟫ record { y = y ; ay = ay ; x=fy = x=fy } = ncn ( subst (λ k → CN k) be13 (UC∋gf ay) ) where + be13 : fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡ x + be13 = begin + fba (fab y (UC⊆a ay)) (b∋fab y (UC⊆a ay)) ≡⟨ fba-eq (sym x=fy) ⟩ + fba (g⁻¹ (be15 lt) (be16 lt)) be19 ≡⟨ g⁻¹-iso (be15 lt) (be16 lt) ⟩ + x ∎ where open ≡-Reasoning be18 : (x y : Ordinal) (ltx : odef (* (& a-UC)) x) (lty : odef (* (& a-UC)) y) → g⁻¹ (be15 ltx) (be16 ltx) ≡ g⁻¹ (be15 lty) (be16 lty) → x ≡ y be18 = ? - be11 : Injection (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC) + be11 : Injection (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC) -- g x 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 + be14 x lt = subst (λ k → odef k (be13 x lt)) (sym *iso) ⟪ a∋fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) , be15 ⟫ 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 = ? + be15 cn with CN.i cn | CN.gfix cn + ... | 0 | a-g ax ¬ib = ⊥-elim (¬ib record { y = _ ; ay = proj1 ( subst (λ k → odef k x) (*iso) lt ) ; x=fy = refl } ) + ... | suc i | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t + = ⊥-elim (be16 (subst (λ k → odef k x) (sym *iso) record { y = y + ; ay = subst (λ k → odef k y) (sym *iso) record { i = i ; gfix = t } ; x=fy = be17 })) where + be17 : x ≡ fab y (UC⊆a (subst (λ k → odef k y) (sym *iso) (record { i = i ; gfix = t }))) + be17 = trans (inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) lt )) (b∋fab y ay) x=fy) (fab-eq refl) 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 = ? + a-UC-iso0 x cx = trans (fba-eq refl) ( g⁻¹-iso (proj1 ( subst (λ k → odef k x) (*iso) cx )) + (λ cn → ⊥-elim (proj2 ( subst (λ k → odef k x) (*iso) cx ) record { i = 0 ; gfix = cn} ) )) - a-UC-iso1 : (x : Ordinal ) → (cx : odef ? x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx) ≡ x - a-UC-iso1 x cx = ? + a-UC-iso1 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) → i→ be10 ( i→ be11 x cx ) (iB be11 x cx) ≡ x + a-UC-iso1 x cx with ODC.p∨¬p O ( IsImage b a g (fba x (proj1 ( subst (λ k → odef k x) (*iso) cx ))) ) + ... | case1 record { y = y ; ay = ay ; x=fy = x=fy } = sym ( inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) cx )) ay x=fy ) + ... | case2 ¬ism = ⊥-elim (¬ism record { y = x ; ay = proj1 ( subst (λ k → odef k x) (*iso) cx ) ; x=fy = refl }) -- C n → f (C n) fU : (x : Ordinal) → ( odef (* (& UC)) x) → Ordinal @@ -280,9 +305,9 @@ ... | (suc i) | next-gf t ix = sym x=fy 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 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ) + h {x} ax with ODC.∋-p O UC (* x) + ... | yes cn = fU x (subst (λ k → odef k x ) (sym *iso) (subst (λ k → CN k) &iso cn) ) + ... | no ncn = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , subst (λ k → ¬ (CN k)) &iso 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) @@ -291,6 +316,35 @@ 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 ( CN 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 CN.i (subst (λ k → odef k x) *iso cn) | CN.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 ⟫ ))) + + 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 + 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 + 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 + be72 x bx with ODC.∋-p O UC (* (h⁻¹ bx)) + be72 x bx | yes cn with ODC.p∨¬p O (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) + be72 x bx | yes cn | case1 record { y = y ; ay = ay ; x=fy = x=fy } with CN.i (subst (λ k → CN k) &iso cn) | CN.gfix (subst (λ k → CN k) &iso cn) + ... | 0 | a-g ax ¬ib = ? + ... | suc i | next-gf ix t = ? + be72 x bx | yes cn | case2 nimg = ? + be72 x bx | no ncn = ? _c<_ : ( A B : HOD ) → Set n A c< B = ¬ ( Injection (& A) (& B) )