Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1478:623b2f792154
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 29 Jun 2024 21:08:29 +0900 |
| parents | 88fdc41868f9 |
| children | 22523e8af390 |
| files | src/OD.agda src/ZProduct.agda src/filter-util.agda |
| diffstat | 3 files changed, 87 insertions(+), 82 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OD.agda Sat Jun 29 15:57:38 2024 +0900 +++ b/src/OD.agda Sat Jun 29 21:08:29 2024 +0900 @@ -44,6 +44,7 @@ ==-sym = HODBase.==-sym O ⇔→== = HODBase.⇔→== O ==-Setoid = HODBase.==-Setoid O +-- use like this open import Relation.Binary.Reasoning.Setoid ==-Setoid -- possible order restriction (required in the axiom of Omega )
--- a/src/ZProduct.agda Sat Jun 29 15:57:38 2024 +0900 +++ b/src/ZProduct.agda Sat Jun 29 21:08:29 2024 +0900 @@ -378,12 +378,12 @@ zp02 {z} eq mab with eq→ m=aB mab ... | ab-pair {w1} {w2} aw1 bw2 = subst (λ k → odef b k ) (proj2 (prod-≡ eq )) bw2 -ZP-proj2-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj2 A B (* z) zab ≡ od∅ → z ≡ & od∅ +ZP-proj2-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj2 A B (* z) zab =h= od∅ → z ≡ & od∅ ZP-proj2-0 {A} {B} {z} {zab} eq = uf10 where uf10 : z ≡ & od∅ uf10 = trans (sym &iso) ( ¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) ) where uf11 : {y : Ordinal } → odef (* z) y → ⊥ - uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ2 pqy)) eq uf12 ) ) where + uf11 {y} zy = ⊥-elim ( ¬x<0 (eq→ eq uf12 ) ) where pqy : odef (ZFP A B) y pqy = zab zy uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) @@ -551,6 +551,10 @@ lemma2 : odef (ZFP B A) (& < * b , * a > ) lemma2 = ZFP→ (subst (λ k → odef B k ) (sym &iso) bb) (subst (λ k → odef A k ) (sym &iso) aa) +ZPmirror-cong : {A B C : HOD} → {cab cab1 : C ⊆ ZFP A B } → ZPmirror A B C cab =h= ZPmirror A B C cab1 +eq→ (ZPmirror-cong {A} {B} {C} {cab} {cab1}) {w} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } +eq← (ZPmirror-cong {A} {B} {C} {cab} {cab1}) {w} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } + ZPmirror-iso : (A B C : HOD) → (cab : C ⊆ ZFP A B ) → ( {x y : HOD} → C ∋ < x , y > → ZPmirror A B C cab ∋ < y , x > ) ∧ ( {x y : HOD} → ZPmirror A B C cab ∋ < y , x > → C ∋ < x , y > ) ZPmirror-iso A B C cab = ⟪ zs00 refl , zs01 ⟫ where @@ -634,12 +638,12 @@ za13 : {x : Ordinal} → ZFProduct B A x → ZPC A B (ZFP A B) (λ x₁ → x₁) x za13 {x} (ab-pair {b} {a} bb aa) = record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ab-pair aa bb ; x=ba = refl } -ZPmirror-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZPmirror A B (* z) zab ≡ od∅ → z ≡ & od∅ +ZPmirror-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → & (ZPmirror A B (* z) zab) ≡ & od∅ → z ≡ & od∅ ZPmirror-0 {A} {B} {z} {zab} eq = trans (sym &iso) uf10 where uf10 : & (* z) ≡ & od∅ uf10 = ¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) where uf11 : {y : Ordinal } → odef (* z) y → ⊥ - uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (& < * (zπ2 pqy) , * (zπ1 pqy) >) ) eq uf12 ) ) where + uf11 {y} zy = ⊥-elim ( ¬x<0 (eq→ (ord→== eq) uf12 ) ) where pqy : odef (ZFP A B) y pqy = zab zy uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >)
--- a/src/filter-util.agda Sat Jun 29 15:57:38 2024 +0900 +++ b/src/filter-util.agda Sat Jun 29 21:08:29 2024 +0900 @@ -167,62 +167,58 @@ isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) fp00 : FQ ⊆ Power Q - fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) ? ) xw - ... | t = ? -- record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb + fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with eq→ *iso ( subst (λ k → odef (* k) w) x=ψz xw ) + ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb f0 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q f1 : {p q : HOD} → Power Q ∋ q → FQ ∋ p → p ⊆ q → FQ ∋ q f1 {p} {q} Qq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP P q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj2 } where PQq : Power (ZFP P Q) ∋ ZFP P q - PQq z zpq = isQ→PxQ {* (& q)} (Qq _) ( subst (λ k → odef k z ) ? zpq ) + PQq z zpq = isQ→PxQ {* (& q)} (Qq _) ( eq→ (ZFP-cong ==-refl (==-sym *iso) ) ( eq→ *iso zpq )) q⊆P : q ⊆ Q - q⊆P {w} qw = Qq _ (subst (λ k → odef k w ) ? qw ) + q⊆P {w} qw = Qq _ (eq← *iso qw ) p⊆P : p ⊆ Q p⊆P {w} pw = q⊆P (p⊆q pw) p=proj2 : & p ≡ & (ZP-proj2 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az))) p=proj2 = x=ψz p⊆ZP : (* z) ⊆ ZFP P p - p⊆ZP = subst (λ k → (* z) ⊆ ZFP P k ) (sym ?) ZP-proj2⊆ZFP + p⊆ZP lt = eq→ (ZFP-cong ==-refl (==-sym ( ord→== p=proj2 )) ) (ZP-proj2⊆ZFP lt) ty05 : filter F ∋ ZFP P p - ty05 = filter1 F (λ z wz → isQ→PxQ p⊆P ?) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP + ty05 = filter1 F (λ z wz → isQ→PxQ p⊆P (eq→ *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP ty06 : ZFP P p ⊆ ZFP P q ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) fp01 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq q=proj2 : & q ≡ & (ZP-proj2 P Q (* (& (ZFP P q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06)))) - q=proj2 = ? -- cong (&) (ZP-proj2=rev (zp1 pqa) q⊆P *iso ) + q=proj2 = ==→o≡ (ZP-proj2=rev (zp1 pqa) q⊆P *iso ) f2 : {p q : HOD} → FQ ∋ p → FQ ∋ q → Power Q ∋ (p ∩ q) → FQ ∋ (p ∩ q) f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq = record { z = _ ; az = ty50 ; x=ψz = pq=proj2 } where p⊆Q : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & (ZP-proj2 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ Q - p⊆Q {zp} {p} fzp p=proj2 {x} px with subst (λ k → odef k x) ? px - ... | t = ? -- record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb + p⊆Q {zp} {p} fzp p=proj2 {x} px with eq→ (ord→== p=proj2) px + ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & (ZP-proj2 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP P p - x⊆pxq {zp} {p} fzp p=proj2 = subst (λ k → (* zp) ⊆ ZFP P k ) (sym ?) ZP-proj2⊆ZFP + x⊆pxq {zp} {p} fzp p=proj2 lt = eq→ (ZFP-cong ==-refl (==-sym ( ord→== p=proj2 )) ) (ZP-proj2⊆ZFP lt) ty54 : Power (ZFP P Q) ∋ (ZFP P p ∩ ZFP P q ) ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where pqz : odef (ZFP P (p ∩ q) ) z - pqz = ? --- subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) )) xz + pqz = eq← (proj2 ZFP∩) (eq→ *iso xz) pqz1 : odef P (zπ1 pqz) pqz1 = zp1 pqz pqz2 : odef Q (zπ2 pqz) pqz2 = p⊆Q fzp x=ψzp (proj1 (zp2 pqz)) ty53 : filter F ∋ ZFP P p - ty53 = filter1 F (λ z wz → isQ→PxQ (p⊆Q fzp x=ψzp) - ?) - ? (x⊆pxq fzp x=ψzp) + ty53 = filter1 F (λ z wz → isQ→PxQ (p⊆Q fzp x=ψzp) (eq→ *iso wz )) (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp) ty52 : filter F ∋ ZFP P q - ty52 = filter1 F (λ z wz → isQ→PxQ (p⊆Q fzq x=ψzq) - ?) - ? (x⊆pxq fzq x=ψzq) + ty52 = filter1 F (λ z wz → isQ→PxQ (p⊆Q fzq x=ψzq) (eq→ *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq) ty51 : filter F ∋ ( ZFP P p ∩ ZFP P q ) ty51 = filter2 F ty53 ty52 ty54 ty50 : filter F ∋ ZFP P (p ∩ q) - ty50 = subst (λ k → filter F ∋ k ) (sym ?) ty51 + ty50 = subst (λ k → odef (filter F) k ) (sym (==→o≡ (proj2 ZFP∩))) ty51 pq=proj2 : & (p ∩ q) ≡ & (ZP-proj2 P Q (* (& (ZFP P (p ∩ q) ))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50))) - pq=proj2 = ? -- cong (&) (ZP-proj2=rev (zp1 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) ? pqx)) *iso ) + pq=proj2 = ==→o≡ (ZP-proj2=rev (zp1 pqa) (λ {x} pqx → Ppq _ (eq← *iso pqx)) *iso ) Filter-Proj2-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) @@ -231,29 +227,31 @@ FQ = Filter-Proj2 pqa F ty60 : ¬ (filter FQ ∋ od∅) ty60 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim (ultra-filter.proper UF - (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) ? x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where + (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (eq→ *iso x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where ty61 : * z ⊆ od∅ - ty61 {x} lt = ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj2-0 (sym ?))) ?) lt )) + ty61 {x} lt = ⊥-elim (¬x<0 ty62 ) where + ty62 : odef od∅ x + ty62 = eq→ *iso (subst (λ k → odef (* k) x) (ZP-proj2-0 (ord→== (sym x=ψz)) ) lt ) ty62 : {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (filter (Filter-Proj2 pqa F) ∋ p) ∨ (filter (Filter-Proj2 pqa F) ∋ (Q ＼ p)) ty62 {p} Qp NEGQ = uf05 where p⊆Q : p ⊆ Q - p⊆Q {z} px = Qp _ (subst (λ k → odef k z) ? px) + p⊆Q {z} px = Qp _ (eq← *iso px) mq : HOD mq = ZFP P p uf03 : Power (ZFP P Q) ∋ mq - uf03 x xz with subst (λ k → odef k x ) ? xz - ... | t = ? -- ab-pair ax by = ab-pair ax (p⊆Q by) + uf03 x xz with eq→ *iso xz + ... | ab-pair ax by = ab-pair ax (p⊆Q by) uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mq) - uf04 x xz = ? -- proj1 (subst (λ k → odef k x) *iso xz) + uf04 x xz = proj1 (eq→ *iso xz) uf02 : (filter F ∋ mq) ∨ (filter F ∋ (ZFP P Q ＼ mq)) uf02 = ultra-filter.ultra UF uf03 uf04 uf05 : (filter FQ ∋ p) ∨ (filter FQ ∋ (Q ＼ p)) uf05 with uf02 - ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = cong (&) ? } - ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = cong (&) ? } + ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = ==→o≡ (ZP-proj2=rev (zp1 pqa) p⊆Q *iso ) } + ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = ==→o≡ (ZP-proj2=rev (zp1 pqa) proj1 (==-trans *iso (proj2 ZFP\Q))) } rcf : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) -rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly } +rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly ; ψ-eq = λ {x} fx1 fx2 → ZPmirror-cong } Filter-sym : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) @@ -264,15 +262,14 @@ fqp = Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf F) fqp<P : fqp ⊆ Power (ZFP Q P) fqp<P {z} record { z = x ; az = fx ; x=ψz = x=ψz } w xw = - ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) - (subst (λ k → odef k w) ? xw) + ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) (eq→ *iso (subst (λ k → odef (* k) w) x=ψz xw)) f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 ; x=ψz = fis05 } where fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q fis00 = filter1 F q⊆ZQP : q ⊆ ZFP Q P - q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) ? qx) + q⊆ZQP {x} qx = QPq _ (eq← *iso qx) p⊆ZQP : p ⊆ ZFP Q P p⊆ZQP {z} px = q⊆ZQP (p⊆q px) fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fqp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fqp)))) @@ -280,26 +277,26 @@ fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP fig03 with Replaced1.az fqp ... | fz = subst (λ k → odef (filter F) k ) fig07 fz where - fig07 : Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (subst (λ k → ? ) ? (p⊆q px)))) - fig07 = trans (sym &iso) ( sym (cong (&) ?)) + fig07 : Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (eq← *iso (p⊆q px)))) + fig07 = trans (sym &iso) (==→o≡ (==-sym ( ZPmirror-rev (ord→== (sym fig06)) )) ) fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP - fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (subst (λ k → odef k x) ? xz) + fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (eq→ *iso xz) fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP fis04 = ZPmirror-⊆ p⊆q fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04)))) - fis05 = cong (&) (sym ?) + fis05 = sym ( ==→o≡ (ZPmirror-rev (==-sym *iso ))) f2 : {p q : HOD} → fqp ∋ p → fqp ∋ q → Power (ZFP Q P) ∋ (p ∩ q) → fqp ∋ (p ∩ q) f2 {p} {q} fp fq QPpq = record { z = _ ; az = fis12 {ZPmirror Q P p p⊆ZQP} {ZPmirror Q P q q⊆ZQP} fig03 fig04 fig01 ; x=ψz = fis05 } where fis12 : {p q : HOD} → filter F ∋ p → filter F ∋ q → Power (ZFP P Q) ∋ (p ∩ q) → filter F ∋ (p ∩ q) fis12 {p} {q} fp fq PQpq = filter2 F fp fq PQpq p⊆ZQP : p ⊆ ZFP Q P - p⊆ZQP {z} px = fqp<P fp _ (subst (λ k → odef k z) ? px) + p⊆ZQP {z} px = fqp<P fp _ (eq← *iso px) q⊆ZQP : q ⊆ ZFP Q P - q⊆ZQP {z} qx = fqp<P fq _ (subst (λ k → odef k z) ? qx) + q⊆ZQP {z} qx = fqp<P fq _ (eq← *iso qx) pq⊆ZQP : (p ∩ q) ⊆ ZFP Q P - pq⊆ZQP {z} pqx = QPpq _ (subst (λ k → odef k z) ? pqx) + pq⊆ZQP {z} pqx = QPpq _ (eq← *iso pqx) fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fp)))) fig06 = Replaced1.x=ψz fp fig09 : & q ≡ & (ZPmirror P Q (* (Replaced1.z fq)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fq)))) @@ -307,16 +304,16 @@ fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP fig03 = subst (λ k → odef (filter F) k ) fig07 ( Replaced1.az fp ) where fig07 : Replaced1.z fp ≡ & (ZPmirror Q P p p⊆ZQP ) - fig07 = trans (sym &iso) ( sym (cong (&) ?)) + fig07 = trans (sym &iso) ( ==→o≡ (==-sym ( ZPmirror-rev (ord→== (sym fig06)) )) ) fig04 : filter F ∋ ZPmirror Q P q q⊆ZQP fig04 = subst (λ k → odef (filter F) k ) fig08 ( Replaced1.az fq ) where fig08 : Replaced1.z fq ≡ & (ZPmirror Q P q q⊆ZQP ) - fig08 = trans (sym &iso) ( sym (cong (&) ?)) + fig08 = trans (sym &iso) ( ==→o≡ (==-sym ( ZPmirror-rev (ord→== (sym fig09)) )) ) fig01 : Power (ZFP P Q) ∋ ( ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP ) - fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP ? + fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (proj2 (eq→ *iso xz)) fis05 : & (p ∩ q) ≡ & (ZPmirror P Q (* (& (ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis12 fig03 fig04 fig01) ))) - fis05 = ? -- cong (&) (sym ( ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} ? )) + fis05 = ==→o≡ (==-sym (ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} (==-trans ZPmirror-∩ (==-sym *iso) ) )) Filter-sym-UF : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) @@ -326,26 +323,40 @@ uf00 : ¬ (Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf F) ∋ od∅) uf00 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) uf10 az )) where uf10 : z ≡ & od∅ - uf10 = ZPmirror-0 (sym ?) + uf10 = ZPmirror-0 (sym x=ψz) uf01 : {p : HOD} → Power (ZFP Q P) ∋ p → Power (ZFP Q P) ∋ (ZFP Q P ＼ p) → (filter FQP ∋ p) ∨ (filter FQP ∋ (ZFP Q P ＼ p)) uf01 {p} QPp NEGP = uf05 where p⊆ZQP : p ⊆ ZFP Q P - p⊆ZQP {z} px = QPp _ (subst (λ k → odef k z) ? px) + p⊆ZQP {z} px = QPp _ (eq← *iso px) mp : HOD mp = ZPmirror Q P p p⊆ZQP uf03 : Power (ZFP P Q) ∋ mp - uf03 x xz = ZPmirror⊆ZFPBA Q P p p⊆ZQP ? + uf03 x xz = ZPmirror⊆ZFPBA Q P p p⊆ZQP (eq→ *iso xz) uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mp) - uf04 x xz = proj1 ? + uf04 x xz = proj1 (eq→ *iso xz) uf02 : (filter F ∋ mp) ∨ (filter F ∋ (ZFP P Q ＼ mp)) uf02 = ultra-filter.ultra UF uf03 uf04 uf05 : (filter FQP ∋ p) ∨ (filter FQP ∋ (ZFP Q P ＼ p)) uf05 with uf02 - ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = ? } - ... | case2 fnp = case2 record { z = _ ; az = uf06 ; x=ψz = ? } where + ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = ==→o≡ (==-sym ( ZPmirror-rev (==-sym *iso) )) } + ... | case2 fnp = case2 record { z = _ ; az = uf06 ; x=ψz = ==→o≡ (==-sym ( ZPmirror-rev (==-sym *iso) )) } where + uf07 : odef (filter F) (& (ZFP P Q ＼ ZPmirror Q P p p⊆ZQP)) + uf07 = fnp + uf08 : (ZFP P Q ＼ ZPmirror Q P p p⊆ZQP) =h= (ZPmirror Q P (ZFP Q P ＼ p) proj1 ) + eq→ uf08 ⟪ ab-pair {a} {b} pa qb , nzm ⟫ = record { a = _ ; b = _ ; aa = qb ; bb = pa + ; c∋ab = ⟪ ab-pair qb pa , nzm1 nzm ⟫ ; x=ba = refl } where + nzm1 : ¬ odef (ZPmirror Q P p p⊆ZQP) (& < * a , * b >) → ¬ odef p (& < * b , * a >) + nzm1 not bap = not record { a = _ ; b = _ ; aa = qb ; bb = pa ; c∋ab = bap ; x=ba = refl } + eq← uf08 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } + = ⟪ subst (λ k → odef (ZFP P Q) k) (sym x=ba) (ab-pair bb aa) , nzm ⟫ where + nzm : ¬ odef (ZPmirror Q P p p⊆ZQP) x + nzm record { a = a1 ; b = b1 ; aa = aa1 ; bb = bb1 ; c∋ab = c∋ab1 ; x=ba = x=ba1 } + = proj2 c∋ab (subst₂ (λ j k → odef p (& < * j , * k >) ) (sym (proj2 peq)) (sym (proj1 peq)) c∋ab1 ) where + peq = prod-≡ (trans (sym x=ba) x=ba1) uf06 : odef (filter F) (& (ZPmirror Q P (ZFP Q P ＼ p) proj1 )) - uf06 = subst (λ k → odef (filter F) k) ? fnp + uf06 = subst (λ k → odef (filter F) k) (==→o≡ uf08) fnp + -- this makes check very slow -- Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → @@ -362,46 +373,35 @@ -- qpa : ZFP Q P ∋ < * (zπ2 pqa) , * (zπ1 pqa) > -- qpa = ab-pair (zp2 pqa) (zp1 pqa) +import Relation.Binary.Reasoning.Setoid as EqS + FPSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → {x : Ordinal } → odef (filter (Filter-Proj1 {P} {Q} pqa F )) x → odef (filter F) (& (ZFP (* x) Q)) FPSet⊆F {P} {Q} {a} pqa F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F uf09 (subst (λ k → odef (filter F) k) (sym &iso) az) uf08 where uf08 : * z ⊆ ZFP (* x) Q - uf08 = subst (λ k → * z ⊆ ZFP k Q) ? ZP-proj1⊆ZFP + uf08 {w} lt = eq→ (ZFP-cong (begin + ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az)) ≈⟨ ==-sym *iso ⟩ + * (& ( ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az)))) ≈⟨ ==-sym (o≡→== x=ψz) ⟩ + * x ∎ ) ==-refl ) ( ZP-proj1⊆ZFP lt ) where + open EqS ==-Setoid uf09 : Power (ZFP P Q) ∋ ZFP (* x) Q - uf09 z xqz = ? -- with subst (λ k → odef k z) *iso xqz - -- ... | ab-pair {c} {d} xc by = ab-pair uf10 by where - -- uf10 : odef P c - -- uf10 with subst (λ k → odef k c) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) xc - -- ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa + uf09 z xqz with eq→ *iso xqz + ... | ab-pair {c} {d} xc by = ab-pair uf10 by where + uf10 : odef P c + uf10 with eq→ *iso (eq→ (o≡→== x=ψz) xc) + ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa FQSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → {x : Ordinal } → odef (filter (Filter-Proj2 {P} {Q} pqa F )) x → odef (filter F) (& (ZFP P (* x) )) FQSet⊆F {P} {Q} {a} pqa F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F uf09 (subst (λ k → odef (filter F) k) (sym &iso) az ) uf08 where uf08 : * z ⊆ ZFP P (* x) - uf08 = subst (λ k → * z ⊆ ZFP P k ) ? ZP-proj2⊆ZFP + uf08 {w} lt = eq→ (ZFP-cong ==-refl (==-trans (==-sym *iso) (==-sym (o≡→== x=ψz)))) ( ZP-proj2⊆ZFP lt ) uf09 : Power (ZFP P Q) ∋ ZFP P (* x) - uf09 z xpz = ? -- with subst (λ k → odef k z) *iso xpz - -- ... | ab-pair {c} {d} ax yc = ab-pair ax uf10 where - -- uf10 : odef Q d - -- uf10 with subst (λ k → odef k d) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) yc - -- ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb - + uf09 z xpz with eq→ *iso xpz + ... | ab-pair {c} {d} ax yc = ab-pair ax uf10 where + uf10 : odef Q d + uf10 with eq→ *iso (eq→ (o≡→== x=ψz) yc) + ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb --- FQSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → --- (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) --- → {x : Ordinal } → odef (filter (Filter-Proj2 {P} {Q} pqa F )) x → odef (filter F) (& (ZFP P (* x) )) ---FQSet⊆F {P} {Q} {a} pqa F {x} f2x = FPSet⊆F {P} {Q} {a} qpa (Filter-sym F) {x} ? where --- qpa : ZFP Q P ∋ < * (zπ2 pqa) , * (zπ1 pqa) > --- qpa = ab-pair (zp2 pqa) (zp1 pqa) - - - - - - - - - -