Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 838:1a5bb940fceb
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 28 Aug 2022 09:15:52 +0900 |
| parents | 8ceaf3455601 |
| children | 710574600659 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 55 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Thu Aug 25 08:19:09 2022 +0900 +++ b/src/zorn.agda Sun Aug 28 09:15:52 2022 +0900 @@ -746,8 +746,27 @@ no-extension ¬sp=x = record { supf = supf1 ; sup = ? ; supf-mono = {!!} ; initial = ? ; chain∋init = ? ; sup=u = ? ; supf-is-sup = ? ; csupf = {!!} ; chain⊆A = λ lt → proj1 lt ; f-next = ? ; f-total = ? } where - pchain0=1 : ? - pchain0=1 = ? + pchain0=1 : pchain ≡ pchain1 + pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where + zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z + zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + zc10 {z} ⟪ az , ch-is-sup u u≤px is-sup fc ⟫ = zc12 fc where + zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z + zc12 (fsuc x fc) with zc12 fc + ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ + zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (ordtrans u≤px (osucc (pxo<x op)) ) ? (init ? ? ) ⟫ + zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z + zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where + zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z + zc13 (fsuc x fc) with zc13 fc + ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ + zc13 (init asu su=z ) with trio< u x + ... | tri< a ¬b ¬c = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u (subst (λ k → u o< k) (sym (Oprev.oprev=x op)) a) ? (init ? ? ) ⟫ + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c ) sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf0 z) sup {z} z≤x with trio< z px ... | tri< a ¬b ¬c = SUP⊆ ? ( ZChain.sup zc (o<→≤ a) ) @@ -829,16 +848,16 @@ ... | tri≈ ¬a b ¬c = ysp ... | tri> ¬a ¬b c = ysp - pchain0 : HOD - pchain0 = UnionCF A f mf ay supf0 x + pchain : HOD + pchain = UnionCF A f mf ay supf0 x - ptotal0 : IsTotalOrderSet pchain0 + ptotal0 : IsTotalOrderSet pchain ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = chain-total A f mf ay supf0 ( (proj2 ca)) ( (proj2 cb)) - usup : SUP A pchain0 - usup = supP pchain0 (λ lt → proj1 lt) ptotal0 + usup : SUP A pchain + usup = supP pchain (λ lt → proj1 lt) ptotal0 spu = & (SUP.sup usup) supf1 : Ordinal → Ordinal @@ -847,23 +866,23 @@ ... | tri≈ ¬a b ¬c = spu ... | tri> ¬a ¬b c = spu - pchain : HOD - pchain = UnionCF A f mf ay supf1 x + pchain1 : HOD + pchain1 = UnionCF A f mf ay supf1 x - pchain⊆A : {y : Ordinal} → odef pchain y → odef A y + pchain⊆A : {y : Ordinal} → odef pchain1 y → odef A y pchain⊆A {y} ny = proj1 ny - pnext : {a : Ordinal} → odef pchain a → odef pchain (f a) + pnext : {a : Ordinal} → odef pchain1 a → odef pchain1 (f a) pnext {a} ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-init (fsuc _ fc) ⟫ pnext {a} ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf a aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ - pinit : {y₁ : Ordinal} → odef pchain y₁ → * y ≤ * y₁ + pinit : {y₁ : Ordinal} → odef pchain1 y₁ → * y ≤ * y₁ pinit {a} ⟪ aa , ua ⟫ with ua ... | ch-init fc = s≤fc y f mf fc ... | ch-is-sup u u≤x is-sup fc = ≤-ftrans (<=to≤ zc7) (s≤fc _ f mf fc) where zc7 : y <= supf1 _ zc7 = ChainP.fcy<sup is-sup (init ay refl) - pcy : odef pchain y + pcy : odef pchain1 y pcy = ⟪ ay , ch-init (init ay refl) ⟫ - ptotal : IsTotalOrderSet pchain + ptotal : IsTotalOrderSet pchain1 ptotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = chain-total A f mf ay supf1 ( (proj2 ca)) ( (proj2 cb)) @@ -884,23 +903,30 @@ ; csupf = {!!} ; chain⊆A = pchain⊆A ; f-next = pnext ; f-total = ptotal } where supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z - UnionCF⊆ : {u : Ordinal} → (a : u o< x ) → UnionCF A f mf ay supf1 u ⊆' UnionCF A f mf ay (supfu a) x - UnionCF⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ - UnionCF⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = {!!} -- with --- UnionCF⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ --- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ --- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ - UnionCFR⊆ : {z : Ordinal} → (a : z o≤ x ) → UnionCF A f mf ay supf1 z ⊆' UnionCF A f mf ay supf1 x - UnionCFR⊆ {u} u<x ⟪ au , ch-init fc ⟫ = ⟪ au , ch-init fc ⟫ - UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (init au1 refl) ⟫ = ⟪ au , ch-is-sup u1 {!!} {!!} (init {!!} {!!}) ⟫ - UnionCFR⊆ {u} u<x ⟪ au , ch-is-sup u1 u1≤x u1-is-sup (fsuc xp fcu1) ⟫ = {!!} -- with --- UnionCF0⊆ {u} u<x ⟪ A∋fc _ f mf fcu1 , ch-is-sup u1 u1≤x u1-is-sup fcu1 ⟫ --- ... | ⟪ aa , ch-init fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-init (fsuc _ fc) ⟫ --- ... | ⟪ aa , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 ( mf _ aa ) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ + pchain0=1 : pchain ≡ pchain1 + pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where + zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z + zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + zc10 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc12 fc where + zc12 : {z : Ordinal} → FClosure A f (supf0 u) z → odef pchain1 z + zc12 (fsuc x fc) with zc12 fc + ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ + zc12 (init asu su=z ) = ⟪ subst (λ k → odef A k) su=z asu , ch-is-sup u u≤x ? (init ? ? ) ⟫ + zc11 : {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z + zc11 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ + zc11 {z} ⟪ az , ch-is-sup u u≤x is-sup fc ⟫ = zc13 fc where + zc13 : {z : Ordinal} → FClosure A f (supf1 u) z → odef pchain z + zc13 (fsuc x fc) with zc13 fc + ... | ⟪ ua1 , ch-init fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-init (fsuc _ fc₁) ⟫ + ... | ⟪ ua1 , ch-is-sup u u≤x is-sup fc₁ ⟫ = ⟪ proj2 ( mf _ ua1) , ch-is-sup u u≤x is-sup (fsuc _ fc₁) ⟫ + zc13 (init asu su=z ) with trio< u x + ... | tri< a ¬b ¬c = ⟪ ? , ch-is-sup u u≤x ? (init ? ? ) ⟫ + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ⊥-elim ( o≤> u≤x c ) sup : {z : Ordinal} → z o≤ x → SUP A (UnionCF A f mf ay supf1 z) sup {z} z≤x with trio< z x - ... | tri< a ¬b ¬c = SUP⊆ (UnionCF⊆ a) (ZChain.sup (pzc (osuc z) {!!}) {!!} ) + ... | tri< a ¬b ¬c = SUP⊆ ? (ZChain.sup (pzc (osuc z) {!!}) {!!} ) ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b c = {!!} sis : {z : Ordinal} (x≤z : z o≤ x) → supf1 z ≡ & (SUP.sup (sup {!!}))