Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 693:a3b7f1e0ca60
same problem again
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 11 Jul 2022 11:49:11 +0900 |
parents | 38103b4e6780 |
children | 196eff771492 |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jul 11 05:50:49 2022 +0900 +++ b/src/zorn.agda Mon Jul 11 11:49:11 2022 +0900 @@ -278,7 +278,7 @@ psup : Ordinal → Ordinal p≤z : (x : Ordinal ) → odef A (psup x) chainf : (x : Ordinal) → HOD - is-chain : (x w : Ordinal) → (x<z : x o< z) → odef (chainf x) w → Chain A f mf ay chainf (psup x) w + is-chain : {x w : Ordinal} → odef (chainf x) w → Chain A f mf ay chainf (psup x) w record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (zc0 : (x : Ordinal) → ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where @@ -307,9 +307,9 @@ -- -- data Chain is total -chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {x y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) +chain-total : (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (chainf : Ordinal → HOD) {s s1 a b : Ordinal } ( ca : Chain A f mf ay chainf s a ) ( cb : Chain A f mf ay chainf s1 b ) → Tri (* a < * b) (* a ≡ * b) (* b < * a ) -chain-total A f mf {x} {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where +chain-total A f mf {y} ay chainf {xa} {xb} {a} {b} ca cb = ct-ind xa xb ca cb where ct-ind : (xa xb : Ordinal) → {a b : Ordinal} → Chain A f mf ay chainf xa a → Chain A f mf ay chainf xb b → Tri (* a < * b) (* a ≡ * b) (* b < * a) ct-ind xa xb {a} {b} (ch-init a fca) (ch-init b fcb) = fcn-cmp y f mf fca fcb ct-ind xa xb {a} {b} (ch-init a fca) (ch-is-sup supb fcb) = tri< ct01 (λ eq → <-irr (case1 (sym eq)) ct01) (λ lt → <-irr (case2 ct01) lt) where @@ -483,7 +483,7 @@ pchain = chainf sc px no-ext : ZChain1 A f mf ay x - no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = is-chain1 } where + no-ext = record { psup = psup1 ; p≤z = p≤z1 ; chainf = chainf1 ; is-chain = ? } where psup1 : Ordinal → Ordinal psup1 z with o≤? z x ... | yes _ = ZChain1.psup sc z @@ -517,15 +517,40 @@ UZ : HOD UZ = UnionCF A x pchainf chainf0 : (z : Ordinal ) → HOD - chainf0 z with o≤? x z - ... | yes _ = UZ - ... | no z<x = ZChain1.chainf (pzc z (o¬≤→< z<x)) z + chainf0 z with trio< z x + ... | tri< a ¬b ¬c = ZChain1.chainf (pzc z a) z + ... | tri≈ ¬a b ¬c = UZ + ... | tri> ¬a ¬b c = UZ + Chain-ext : {s a : Ordinal} → (ca : odef UZ a) + → Chain A f mf ay ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca)))) s a → Chain A f mf ay chainf0 s a + Chain-ext {s} {a} ca (ch-init a x) = ch-init a x + Chain-ext {s} {a} ca (ch-is-sup is-sup fc) = ch-is-sup sc5 fc where + sc7 : odef ( ZChain1.chainf (pzc _ (UChain.u<x (proj2 ca))) s ) a + sc7 = ChainP.csupz is-sup + sc8 : (z<x : s o< x ) → chainf0 s ≡ ( ZChain1.chainf (pzc _ z<x )) s + sc8 z<x with trio< s x + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? + ... | tri< a ¬b ¬c with o<-irr a z<x + ... | refl = refl + sc6 : odef (chainf0 s) a + sc6 with trio< s x + ... | tri≈ ¬a b ¬c = ? + ... | tri> ¬a ¬b c = ? + ... | tri< a' ¬b ¬c with o<-irr a' ? -- (UChain.u<x (proj2 ca)) + ... | eq = ? -- ChainP.csupz is-sup + sc5 : ChainP A f mf ay chainf0 s a + sc5 = record { + asup = ChainP.asup is-sup + ; fcy<sup = ChainP.fcy<sup is-sup + ; csupz = sc6 + ; order = ? } total-UZ : IsTotalOrderSet UZ total-UZ {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 chainf0 {!!} {!!} - -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) _ _ (UChain.chain∋z (proj2 ca))) - -- (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) _ _ (UChain.chain∋z (proj2 cb))) + uz01 = chain-total A f mf ay chainf0 + (Chain-ext ca (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 ca))) (UChain.chain∋z (proj2 ca)))) + (Chain-ext cb (ZChain1.is-chain (pzc _ (UChain.u<x (proj2 cb))) (UChain.chain∋z (proj2 cb)))) usup : SUP A UZ usup = supP UZ (λ lt → proj1 lt) total-UZ spu = & (SUP.sup usup)