# HG changeset patch # User Shinji KONO # Date 1688194234 -32400 # Node ID a444ea176011272deeae40b1dfd9c38600b63c85 # Parent 77a3de21ee50e7deeb186008b0a5e48a53a5cfdd ... diff -r 77a3de21ee50 -r a444ea176011 src/cardinal.agda --- a/src/cardinal.agda Sat Jul 01 14:26:20 2023 +0900 +++ b/src/cardinal.agda Sat Jul 01 15:50:34 2023 +0900 @@ -197,14 +197,19 @@ g⁻¹-iso1 : {x : Ordinal } → (bx : odef (* b) x) → (nc0 : IsImage b a g (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) + g⁻¹-eq : {x : Ordinal } → (ax ax' : odef (* a) x) → {nc0 nc0' : IsImage b a g x } → g⁻¹ ax nc0 ≡ g⁻¹ ax' nc0' + g⁻¹-eq {x} ax ax' {record { y = y₁ ; ay = ay₁ ; x=fy = x=fy₁ }} {record { y = y ; ay = ay ; x=fy = x=fy }} + = inject g _ _ ay₁ ay (trans (sym x=fy₁) x=fy ) + + be15 : {x : Ordinal } → odef (* (& a-UC)) x → odef (* a) x + be15 {x} lt with subst (λ k → odef k x) *iso lt + ... | ⟪ ax , ncn ⟫ = ax + be16 : {x : Ordinal } → odef (* (& a-UC)) x → IsImage b a g x + be16 {x} lt with subst (λ k → odef k x) *iso lt + ... | ⟪ ax , ncn ⟫ = nimg ax ncn + 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 - ... | ⟪ ax , ncn ⟫ = ax - be16 : {x : Ordinal } → odef (* (& a-UC)) x → IsImage b a g x - be16 {x} lt with subst (λ k → odef k x) *iso lt - ... | ⟪ ax , ncn ⟫ = nimg ax ncn be17 : (x : Ordinal) (lt : odef (* (& a-UC)) x) → odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) (g⁻¹ (be15 lt) (be16 lt)) 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 @@ -227,14 +232,14 @@ 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 )) , be15 ⟫ where - be16 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) - be16 = proj2 ( subst (λ k → odef k x) (*iso) lt ) - be15 : ¬ gfImage (be13 x lt) - be15 cn with cn + be14 x lt = subst (λ k → odef k (be13 x lt)) (sym *iso) ⟪ a∋fba x ( proj1 ( subst (λ k → odef k x) (*iso) lt )) , be25 ⟫ where + be26 : ¬ (odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x) + be26 = proj2 ( subst (λ k → odef k x) (*iso) lt ) + be25 : ¬ gfImage (be13 x lt) + be25 cn with cn ... | a-g ax ¬ib = ⊥-elim (¬ib record { y = _ ; ay = proj1 ( subst (λ k → odef k x) (*iso) lt ) ; x=fy = refl } ) ... | next-gf record { y = y ; ay = ay ; x=fy = x=fy } t - = ⊥-elim (be16 (subst (λ k → odef k x) (sym *iso) record { y = y + = ⊥-elim (be26 (subst (λ k → odef k x) (sym *iso) record { y = y ; ay = subst (λ k → odef k y) (sym *iso) t ; x=fy = be17 })) where be17 : x ≡ fab y (UC⊆a (subst (λ k → odef k y) (sym *iso) t)) be17 = trans (inject g _ _ (proj1 ( subst (λ k → odef k x) (*iso) lt )) (b∋fab y ay) x=fy) (fab-eq refl) @@ -250,7 +255,9 @@ a-UC-iso11 : (x : Ordinal ) → (cx : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x ) → (ib : odef (* (& a-UC)) (fba x ( proj1 ( subst (λ k → odef k x) (*iso) cx )) )) → i→ be10 ( i→ be11 x cx ) ib ≡ x - a-UC-iso11 x cx ib = trans ? (a-UC-iso1 x cx) + a-UC-iso11 x cx ib 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 @@ -416,21 +423,14 @@ ... | 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 = ? where -- a-UC-iso11 x be79 (subst (λ k → odef k (fba x (proj1 (subst (λ k₁ → odef k₁ x) *iso be79 ) ))) (sym *iso) be77 ) where - be79 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )) )) x - be79 = proj1 (subst (λ k → odef k x) *iso (subst (λ k → odef k x) (sym *iso) ⟪ bx , subst (λ k → odef k x → ⊥) (sym *iso) x₁ ⟫)) - bx1 : odef (* b) x - bx1 = proj1 (subst (λ k → odef k x) *iso be79) - be77 : odef a-UC (fba x bx1 ) - be77 = subst (λ k → odef k (fba x bx)) *iso (subst (λ k → odef k (fba x bx)) (sym *iso) ⟪ bx , subst (λ k → odef k (fba x bx) → ⊥) (sym *iso) x₁ ⟫) - be80 : odef (* (& a-UC)) (fba x bx1 ) - be80 = - (subst (λ k → odef k (fba x (proj1 (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso) - ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫))))) - (sym *iso) - ⟪ proj1 (subst₂ (λ A → OD.def (od A)) *iso refl (subst (λ k → OD.def (od k) (fba x (proj1 - (subst (λ k₁ → OD.def (od k₁) x) *iso (subst (λ k₁ → OD.def (od k₁) x) (sym *iso) - ⟪ bx , subst (λ k₁ → OD.def (od k₁) x → ⊥) (sym *iso) x₁ ⟫))))) (sym *iso) ⟪ a∋fba x (proj1 (subst (λ k → OD.def (od k) x) *iso (subst (λ k → OD.def (od k) x) (sym *iso) ⟪ bx , subst (λ k → OD.def (od k) x → ⊥) (sym *iso) x₁ ⟫))) , ? ⟫)) , c2 ⟫) + ... | case2 c2 = a-UC-iso11 x be76 be77 where + be76 : odef (* (b - & (Image (& UC) (Injection-⊆ UC⊆a f)))) x + be76 = subst (λ k → odef k x) (sym *iso) ⟪ bx , (λ lt → subst (λ k → odef k x → ⊥) (sym *iso) x₁ lt ) ⟫ + be77 : odef (* (& a-UC)) (fba x (proj1 (subst (λ k → odef k x) *iso be76))) + be77 = subst (λ k → odef k (fba x (proj1 (subst (λ k → odef k x) *iso be76)) )) (sym *iso) + ⟪ a∋fba x (proj1 (subst (λ k → odef k x) *iso be76)) , ? ⟫ + + 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