Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1406:ba377f7d0c40
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Jun 2023 16:58:43 +0900 |
| parents | 6db21bb5e704 |
| children | 523bd51605cb |
| files | src/cardinal.agda |
| diffstat | 1 files changed, 19 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/cardinal.agda Thu Jun 29 11:17:20 2023 +0900 +++ b/src/cardinal.agda Thu Jun 29 16:58:43 2023 +0900 @@ -271,37 +271,31 @@ ... | 0 | a-g ax ¬ib = sym x=fy ... | (suc i) | next-gf t ix = sym x=fy - -- be11 : Injection (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) ))) (& a-UC) - Img∨ : (x : Ordinal) → (bx : odef (* b) x) → odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x - ∨ odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x - Img∨ x bx = be20 where - be20 : odef (* (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x ∨ odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x - be20 with ∨L＼X {* a} {UC} (a∋fba x bx) - ... | case1 uc = case1 (subst (λ k → odef k x) (sym *iso) be21 ) where - be21 : odef (Image (& UC) (Injection-⊆ UC⊆a f)) x - be21 with CN.i uc | CN.gfix uc - ... | 0 | a-g ax ¬ib = ⊥-elim (¬ib record { y = x ; ay = bx ; x=fy = refl } ) - ... | suc i | next-gf {x1} {y1} record { y = y ; ay = ay ; x=fy = x=fy } t - = record { y = y ; ay = subst (λ k → odef k y) (sym *iso) be25 ; x=fy = trans be24 (fab-eq refl) } where - be24 : x ≡ fab y ay - be24 = inject g _ _ bx (b∋fab y ay) x=fy - be25 : odef UC y - be25 = record { i = i ; gfix = t } - be20 | case2 ⟪ agx , ncn ⟫ = case2 be21 where - be22 : ¬ odef (C 0) (fba x bx) -- condition for g⁻¹ - be22 = λ nc0 → ncn record { i = 0 ; gfix = nc0 } - be21 : odef (* (b - (& (Image (& UC) (Injection-⊆ UC⊆a f) )))) x - be21 = ? - 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 : Ordinal } → (bx : odef (* b) x) → Ordinal - h⁻¹ {x} bx with ODC.p∨¬p O ( CN x ) - ... | case1 cn = fU x (subst (λ k → odef k x ) (sym *iso) cn ) - ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) ? ) + h⁻¹ {x} bx with ODC.p∨¬p O ( CN (fba x bx )) + ... | case1 cn = be63 where -- Uf x (subst (λ k → odef k x ) (sym *iso) record { y = _ ; ay = ? ; x=fy = ? } ) + be63 : Ordinal + be63 with CN.i cn | CN.gfix cn + ... | 0 | a-g ax ¬ib = Uf x (subst (λ k → odef k x ) (sym *iso) record { y = _ ; ay = ? ; x=fy = ? } ) + ... | suc i | next-gf {px} ix t = Uf (fab px ?) (subst (λ k → odef k (fab px ?) ) (sym *iso) + record { y = _ ; ay = subst (λ k → odef k (fab px ?)) (sym *iso) record { i = ? ; gfix = ? } ; x=fy = ? } ) + ... | case2 ncn = i→ be11 x (subst (λ k → odef k x ) (sym *iso) be60 ) where + be61 : ¬ odef (Image (& UC) (Injection-⊆ UC⊆a f)) x + be61 record { y = y ; ay = ay ; x=fy = x=fy } = be62 where + cny : CN y + cny = subst (λ k → odef k y ) *iso ay + be62 : ⊥ + be62 with CN.i cny | CN.gfix cny + ... | 0 | a-g ax ¬ib = ncn record { i = 1 ; gfix = next-gf record { y = _ ; ay = ax ; x=fy = fba-eq x=fy } (a-g ax ¬ib) } + ... | suc i | t = ncn record { i = suc (suc i) ; gfix = next-gf record { y = _ ; ay = ? ; x=fy = fba-eq x=fy } t } + be60 : odef (* b ＼ * (& (Image (& UC) (Injection-⊆ UC⊆a f)))) x + be60 = ⟪ bx , subst (λ k → ¬ odef k x ) (sym *iso) be61 ⟫ + _c<_ : ( A B : HOD ) → Set n A c< B = ¬ ( Injection (& A) (& B) )