Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1240:fbe072447243

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Mar 2023 13:02:09 +0900
parents 5223f0b40d91
children 5f1572d1f19a
files src/generic-filter.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Sun Mar 12 11:58:55 2023 +0900
+++ b/src/generic-filter.agda	Sun Mar 12 13:02:09 2023 +0900
@@ -162,7 +162,7 @@
 P-GenericFilter : (P L p0 : HOD ) → (LP : L ⊆ Power P) → L ∋ p0 → (C : CountableModel ) → GenericFilter {L} {P} LP ( ctl-M C )
 P-GenericFilter P L p0 L⊆PP Lp0 C = record {
       genf = record { filter = Replace (PDHOD L p0 C) (λ x → P ＼ x)  ; f⊆L =  ? ; filter1 = ? ; filter2 = ? }
-    ; generic = ?
+    ; generic = λ D cd → subst (λ k → ¬ (Dense.dense D ∩ k) ≡ od∅ ) (sym gf00) (fdense D cd )
    } where
         f⊆PL :  PDHOD L p0 C ⊆ L 
         f⊆PL lt = x∈PP lt  
@@ -173,9 +173,9 @@
         ... | tri< a ¬b ¬c = ?
         ... | tri≈ ¬a eq ¬c = ?
         ... | tri> ¬a ¬b c = ? 
-        gf : HOD
-        gf  = Replace (Replace (PDHOD L p0 C) (λ x → P ＼ x)) (_＼_ P)
-        fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D  → ¬ (Dense.dense D ∩ gf ) ≡ od∅
+        gf00 : Replace (Replace (PDHOD L p0 C) (λ x → P ＼ x)) (_＼_ P) ≡ PDHOD L p0 C
+        gf00 = ?
+        fdense : (D : Dense {L} {P} L⊆PP ) → (ctl-M C ) ∋ Dense.dense D  → ¬ (Dense.dense D ∩ (PDHOD L p0 C)) ≡ od∅
         fdense D MD eq0  = ? where
            open Dense