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

changeset 1259:4993a95d3fc8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... filter definition
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Mar 2023 11:33:20 +0900
parents 04fc80af6f77
children 8a8052df5254
files src/generic-filter.agda
diffstat 1 files changed, 17 insertions(+), 17 deletions(-) [+]
line wrap: on
line diff
--- a/src/generic-filter.agda	Fri Mar 17 00:33:43 2023 +0900
+++ b/src/generic-filter.agda	Fri Mar 17 11:33:20 2023 +0900
@@ -152,15 +152,15 @@
 
 record Expansion  (L : HOD) {p : HOD } (dense : HOD) (Lp : L ∋ p) : Set (Level.suc n) where
    field
-       expansion : HOD
-       dense∋exp : dense ∋ expansion 
-       p⊆exp : p ⊆ expansion 
+       exp : HOD
+       D∋exp : dense ∋ exp 
+       p⊆exp : p ⊆ exp 
 
 record Dense  {L P : HOD } (LP : L ⊆ Power P)  : Set (Level.suc n) where
    field
        dense : HOD
        d⊆P :  dense ⊆ L
-       has-expansion : {p : HOD} → (Lp : L ∋ p) → Expansion L dense Lp
+       has-exp : {p : HOD} → (Lp : L ∋ p) → Expansion L dense Lp
 
 record GenericFilter {L P : HOD} (LP : L ⊆ Power P) (M : HOD) : Set (Level.suc n) where
     field
@@ -241,14 +241,14 @@
            ... | yes y = ⊥-elim ( ¬x<0 ( _==_.eq→ fd10 fd21 ) ) where
               L∋pn : L ∋ * (find-p L C an (& p0))
               L∋pn = subst (λ k → odef L k) (sym &iso) (fd09 an )
-              exp = has-expansion D L∋pn
-              L∋df : L ∋ ( expansion exp )
-              L∋df = (d⊆P D) (dense∋exp exp)
-              pn∋df : (* (ctl→ C an)) ∋ ( expansion exp)
-              pn∋df = subst (λ k → odef k (& ( expansion exp))) d=an (dense∋exp exp )
-              pn⊆df : (y : Ordinal) → odef (* (find-p L C an (& p0))) y → odef (* (& (expansion exp))) y
-              pn⊆df y py = subst (λ k → odef k y ) (sym *iso) (p⊆exp exp py)
-              fd21 : odef (PGHOD an L C (find-p L C an (& p0)) ) (& (expansion exp))
+              ex = has-exp D L∋pn
+              L∋df : L ∋ ( exp ex )
+              L∋df = (d⊆P D) (D∋exp ex)
+              pn∋df : (* (ctl→ C an)) ∋ ( exp ex)
+              pn∋df = subst (λ k → odef k (& ( exp ex))) d=an (D∋exp ex )
+              pn⊆df : (y : Ordinal) → odef (* (find-p L C an (& p0))) y → odef (* (& (exp ex))) y
+              pn⊆df y py = subst (λ k → odef k y ) (sym *iso) (p⊆exp ex py)
+              fd21 : odef (PGHOD an L C (find-p L C an (& p0)) ) (& (exp ex))
               fd21 = ⟪ L∋df , ⟪ pn∋df , pn⊆df ⟫ ⟫
               fd10 :  PGHOD an L C (find-p L C an (& p0)) =h= od∅
               fd10 = ≡o∅→=od∅ y
@@ -297,22 +297,22 @@
     D⊆PP : D ⊆ Power P
     D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
     DD : Dense {L} {P} LPP
-    DD = record { dense = D ; d⊆P = proj1 ; has-expansion = exp } where
+    DD = record { dense = D ; d⊆P = proj1 ; has-exp = exp } where
         exp : {p : HOD} → (Lp : L ∋ p) → Expansion L D Lp
         exp {p} Lp = exp1 where
             q : HOD
             q = NotCompatible.q (NC Lp)
             r : HOD
             r = NotCompatible.r (NC Lp)
-            Lr : L ∋ r
-            Lr = NotCompatible.Lr (NC Lp)
             Lq : L ∋ q
             Lq = NotCompatible.Lq (NC Lp)
+            Lr : L ∋ r
+            Lr = NotCompatible.Lr (NC Lp)
             exp1 : Expansion L D Lp
             exp1  with ODC.p∨¬p O (rgf ∋ q)
-            ... | case2 ngq = record { expansion = q  ; dense∋exp = ⟪ Lq , ngq ⟫ ; p⊆exp = NotCompatible.p⊆q (NC Lp)}  
+            ... | case2 ngq = record { exp = q  ; D∋exp = ⟪ Lq , ngq ⟫ ; p⊆exp = NotCompatible.p⊆q (NC Lp)}  
             ... | case1 gq with ODC.p∨¬p O (rgf ∋ r)
-            ... | case2 ngr = record { expansion = r  ; dense∋exp = ⟪ Lr , ngr ⟫ ; p⊆exp = NotCompatible.p⊆r (NC Lp)}  
+            ... | case2 ngr = record { exp = r  ; D∋exp = ⟪ Lr , ngr ⟫ ; p⊆exp = NotCompatible.p⊆r (NC Lp)}  
             ... | case1 gr = ⊥-elim ( ll02 ⟪ ? , ? ⟫ ) where
                 ll02 : ¬ ( (q ⊆ p) ∧ (r ⊆ p) )
                 ll02 = NotCompatible.¬compat (NC Lp) p ?