# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1679020400 -32400
# Node ID 4993a95d3fc8d8db90596c7c3e62b05ab4254aa3
# Parent  04fc80af6f77a693320f0953e0d669cdbc82a52d
... filter definition

diff -r 04fc80af6f77 -r 4993a95d3fc8 src/generic-filter.agda
--- 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 ?