# HG changeset patch # User Shinji KONO # Date 1688207874 -32400 # Node ID f2125be6fec1ed1a0644715a4f7e91af12f0a2ee # Parent 5f22e830e46047d1f32bb45cd43eb2d9888bafc5 ... diff -r 5f22e830e460 -r f2125be6fec1 src/cardinal.agda --- a/src/cardinal.agda Sat Jul 01 18:19:34 2023 +0900 +++ b/src/cardinal.agda Sat Jul 01 19:37:54 2023 +0900 @@ -124,8 +124,8 @@ 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 (cc0 x) - ; fun→ = λ x lt → h⁻¹ lt (cc1 x) + 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)) @@ -158,6 +158,7 @@ aucimg : {x : Ordinal } → (cx : odef (* (& a-UC)) x ) → IsImage b a g x aucimg {x} cx with subst (λ k → odef k x ) *iso cx + ... | ⟪ ax , ncn ⟫ = nimg ax ncn -- UC ⊆ * a @@ -208,10 +209,17 @@ be16 {x} lt with subst (λ k → odef k x) *iso lt ... | ⟪ ax , ncn ⟫ = nimg ax ncn - cc11-case2 : {x : Ordinal} (ax : odef (* a) x) → (x₁ : ¬ gfImage x) - → ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) (g⁻¹ (be15 (subst (λ k → odef k x) (sym *iso) ⟪ ax , x₁ ⟫)) - (be16 (subst (λ k → odef k x) (sym *iso) ⟪ ax , x₁ ⟫))) - cc11-case2 {x} ax gfi = ? + nimg1 : {x : Ordinal} (ax : odef (* a) x) → (ncn : ¬ gfImage x) → IsImage b a g x + nimg1 {x} ax ncn = nimg ax ncn + + 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 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 @@ -330,22 +338,22 @@ → (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) → Set n - CC0 x = gfImage x ∨ (¬ gfImage x) + CC0 : (x : Ordinal) → (bx : odef (* a) x) → Set n + CC0 x ax = gfImage x ∨ (¬ gfImage x) - CC1 : (x : Ordinal) → Set n - CC1 x = odef (Image (& UC) (Injection-⊆ UC⊆a f)) x ∨ (¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x) + CC1 : (x : Ordinal) → (bx : odef (* b) x) → Set n + CC1 x bx = gfImage (fba x bx) ∨ (¬ gfImage (fba x bx) ) - cc0 : (x : Ordinal) → CC0 x + cc0 : (x : Ordinal) → CC0 x ? cc0 x = ODC.p∨¬p O (gfImage x) - cc1 : (x : Ordinal) → CC1 x - cc1 x = ODC.p∨¬p O (odef (Image (& UC) (Injection-⊆ UC⊆a f)) x) + cc1 : (x : Ordinal) → (bx : odef (* b) x) → CC1 x ? + cc1 x bx = ODC.p∨¬p O (gfImage (fba x bx) ) - cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt ) + cc20 : {x : Ordinal } → (lt : odef (* b) x) → CC0 (fba x lt ) ? cc20 = ? - cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) + cc21 : {x : Ordinal } → (lt : odef (* a) x) → CC1 (fab x lt ) ? cc21 = ? -- @@ -360,22 +368,21 @@ -- -- otherwise not strict positive on gfImage error will happen - h : {x : Ordinal } → (ax : odef (* a) x) → gfImage x ∨ (¬ gfImage x) → Ordinal + 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} ax (case2 ncn) = i→ be10 x (subst (λ k → odef k x ) (sym *iso) ⟪ ax , ncn ⟫ ) + 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} bx ( case2 ncn) = fba x bx - 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 bx ncn) ) -- ¬ x ≡ f y + 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 ? ) - cc10 : {x : Ordinal} → (bx : odef (* b) x) → (cc1 : CC1 x) → 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 x₁ ) - - cc11 : {x : Ordinal} → (ax : odef (* a) x) → (cc0 : CC0 x) → CC1 (h ax cc0 ) - cc11 {x} bx (case1 x₁) = case1 (subst₂ (λ j k → odef j k ) *iso refl (be04 (subst (λ k → odef k x) (sym *iso) x₁))) - cc11 {x} bx (case2 x₁) = case2 (cc11-case2 bx x₁) + 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₁) 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 @@ -384,11 +391,11 @@ ... | 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 ⟫ ))) + 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) → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) ∨ ( ¬ (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x) )) - → odef (* a) (h⁻¹ bx or ) + → 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 @@ -397,7 +404,7 @@ be71-1 : (x : Ordinal) (bx : odef (* b) x) → (or : (odef ( Image (& UC) (Injection-⊆ UC⊆a f)) x)) - → gfImage (h⁻¹ bx (case1 or) ) + → 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)) be70-1 : (x : Ordinal) (lt : odef (* a) x) → (or : gfImage x ∨ (¬ gfImage x )) → odef ( Image (& UC) (Injection-⊆ UC⊆a f)) (h lt or ) @@ -409,10 +416,8 @@ ... | case2 lt1 with iB be10 ? ? ... | t = ? - be75 : (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx (cc1 x)) - be75 x lt with cc1 x - ... | case1 lt1 = ? - ... | case2 lt1 = ? + be75 : (x : Ordinal) (bx : odef (* b) x) → odef (* a) (h⁻¹ bx ? ) + be75 x lt = ? fba-image : {x : Ordinal } → (bx : odef (* b) x) → odef (Image b g) (fba x bx) fba-image {x} bx = record { y = _ ; ay = bx ; x=fy = refl } @@ -420,34 +425,12 @@ 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) → h (be71 x bx cc1 ) (cc10 bx cc1) ≡ x - be72 x bx (case1 (x₁ @ record { y = y ; ay = ay ; x=fy = x=fy })) = ? where - -- UC-iso11 x be76 - -- (subst (λ k → odef k (IsImage.y (subst (λ k → odef k x) *iso be76))) (sym *iso) be77 ) where - be76 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x - be76 = subst (λ k → odef k x) (sym *iso) x₁ - be78 : y ≡ IsImage.y (subst (λ k → odef k x) *iso be76) - be78 = ImageUnique x₁ (subst (λ k → odef k x) *iso be76) - be77 : odef UC (IsImage.y (subst (λ k → odef k x) *iso be76)) - be77 = subst₂ (λ j k → odef j k ) *iso be78 ay - be72 x bx (case2 x₁) with cc10 bx (case2 x₁) - ... | case1 (a-g ax ¬ib) = ⊥-elim (¬ib record { y = x ; ay = bx ; x=fy = (fba-eq refl) } ) - ... | case1 (next-gf record { y = y ; ay = ay ; x=fy = x=fy } c1) - = ⊥-elim (x₁ record { y = y ; ay = subst (λ k → odef k y) (sym *iso) c1 - ; x=fy = inject g _ _ _ (b∋fab y _) (trans x=fy (fba-eq (fab-eq refl))) }) - ... | case2 c2 with nimg (a∋fba x bx) (subst (λ k → gfImage (fba x k) → ⊥) ? c2 ) - ... | record { y = y ; ay = ay ; x=fy = x=fy } = sym (inject g _ _ ? ? ?) + be72 : (x : Ordinal) (bx : odef (* b) x) → (cc1 : CC1 x bx) → h (be71 x bx ? ) (cc10 bx ? ) ≡ x + be72 x bx = ? - be73 : (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ) → h⁻¹ (be70 x ax cc0) (cc11 ax cc0) ≡ x - be73 x ax (case1 x₁) with cc11 ax (case1 x₁) - ... | case1 c1 = trans ? be76 where - be76 : IsImage.y (subst (λ k → odef k (fU x (subst (λ k₁ → odef k₁ x) (sym *iso) x₁))) *iso (be04 (subst (λ k → odef k x) (sym *iso) x₁))) ≡ x - be76 = UC-iso0 x (subst (λ k → odef k x) (sym *iso) x₁ ) - ... | case2 c2 = ? - be73 x ax (case2 x₁) with cc11 ax (case2 x₁) - ... | case1 c1 = ⊥-elim ( x₁ ? ) - ... | case2 c2 = trans ? (a-UC-iso0 x ? ) + be73 : (x : Ordinal) (ax : odef (* a) x) → (cc0 : CC0 x ax ) → h⁻¹ (be70 x ax cc0) ? ≡ x + be73 x ax (case1 x₁) = ? _c<_ : ( A B : HOD ) → Set n