Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1010:f80d525e6a6b
Recursive record IChain
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 20 Nov 2022 17:33:10 +0900 |
parents | 7c39cae23803 |
children | 66154af40f89 |
files | src/zorn.agda |
diffstat | 1 files changed, 37 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Sun Nov 20 16:07:25 2022 +0900 +++ b/src/zorn.agda Sun Nov 20 17:33:10 2022 +0900 @@ -1304,22 +1304,36 @@ ysp = MinSUP.sup (ysup f mf ay) - supf0 : Ordinal → Ordinal - supf0 z with trio< z x - ... | tri< a ¬b ¬c = ZChain.supf (pzc (ob<x lim a)) z - ... | tri≈ ¬a b ¬c = ysp - ... | tri> ¬a ¬b c = ysp + supfz : {z : Ordinal } → z o< x → Ordinal + supfz {z} z<x = ZChain.supf (pzc (ob<x lim z<x)) z + + record IChain (supfz : {z : Ordinal } → z o< x → Ordinal) (z : Ordinal ) : Set n where + field + i : Ordinal + i<x : i o< x + fc : FClosure A f (supfz i<x) z + + pchainx : HOD + pchainx = record { od = record { def = λ z → IChain supfz z } ; odmax = & A ; <odmax = zc00 } where + zc00 : {z : Ordinal } → IChain supfz z → z o< & A + zc00 {z} ic = z09 ( A∋fc (supfz (IChain.i<x ic)) f mf (IChain.fc ic) ) - pchain : HOD - pchain = UnionCF A f mf ay supf0 x + zeq : {xa xb z : Ordinal } + → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa + → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z + zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = spuf-unique A f mf ay xa≤xb + (pzc xa<x) (pzc xb<x) z≤xa - ptotal0 : IsTotalOrderSet pchain - ptotal0 {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + ptotalx : IsTotalOrderSet pchainx + ptotalx {a} {b} ia ib = 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)) + uz01 with trio< (IChain.i ia) (IChain.i ib) + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? - usup : MinSUP A pchain - usup = minsupP pchain (λ lt → proj1 lt) ptotal0 + usup : MinSUP A pchainx + usup = minsupP pchainx (λ lt → ? ) ptotalx spu = MinSUP.sup usup supf1 : Ordinal → Ordinal @@ -1328,14 +1342,15 @@ ... | tri≈ ¬a b ¬c = spu ... | tri> ¬a ¬b c = spu - pchain1 : HOD - pchain1 = UnionCF A f mf ay supf1 x + pchain : HOD + pchain = UnionCF A f mf ay supf1 x + + -- pchain ⊆ pchainx - zeq : {xa xb z : Ordinal } - → (xa<x : xa o< x) → (xb<x : xb o< x) → xa o≤ xb → z o≤ xa - → ZChain.supf (pzc xa<x) z ≡ ZChain.supf (pzc xb<x) z - zeq {xa} {xb} {z} xa<x xb<x xa≤xb z≤xa = spuf-unique A f mf ay xa≤xb - (pzc xa<x) (pzc xb<x) z≤xa + ptotal : IsTotalOrderSet pchain + 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)) sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc (ob<x lim a)) z sf1=sf {z} z<x with trio< z x @@ -1349,9 +1364,9 @@ ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = refl - zc11 : {z : Ordinal } → (a : z o< x ) → odef pchain (ZChain.supf (pzc (ob<x lim a)) z) - zc11 {z} z<x = ⟪ ZChain.asupf (pzc (ob<x lim z<x)) , ch-is-sup (ZChain.supf (pzc (ob<x lim z<x)) z) - ? ? (init ? ?) ⟫ + -- zc11 : {z : Ordinal } → (a : z o< x ) → odef pchain (ZChain.supf (pzc (ob<x lim a)) z) + -- zc11 {z} z<x = ⟪ ZChain.asupf (pzc (ob<x lim z<x)) , ch-is-sup (ZChain.supf (pzc (ob<x lim z<x)) z) + -- ? ? (init ? ?) ⟫ sfpx<=spu : {z : Ordinal } → supf1 z <= spu sfpx<=spu {z} with trio< z x