# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1679267770 -32400
# Node ID 48d37da9833159478da75ded2942e98f7567b14a
# Parent  440ebaf9f70759fa69874a6d3036ee4bee1d58bf
...

diff -r 440ebaf9f707 -r 48d37da98331 src/generic-filter.agda
--- a/src/generic-filter.agda	Mon Mar 20 08:15:10 2023 +0900
+++ b/src/generic-filter.agda	Mon Mar 20 08:16:10 2023 +0900
@@ -153,26 +153,26 @@
 record Expansion  (p : HOD) (dense : HOD)  : Set (Level.suc n) where
    field
        exp : HOD
-       D∋exp : dense ∋ exp 
-       p⊆exp : p ⊆ exp 
+       D∋exp : dense ∋ exp
+       p⊆exp : p ⊆ exp
 
 record Dense  (L : HOD ) : Set (Level.suc n) where
    field
        dense : HOD
        d⊆P :  dense ⊆ L
-       has-exp : {p : HOD} → (Lp : L ∋ p) → Expansion p dense 
+       has-exp : {p : HOD} → (Lp : L ∋ p) → Expansion p dense
 
 record Exp2 (I : HOD)  ( p q : HOD ) : Set (Level.suc n) where
-   field 
+   field
        exp : HOD
-       I∋exp : I ∋ exp 
-       p⊆exp : p ⊆ exp 
-       q⊆exp : q ⊆ exp 
+       I∋exp : I ∋ exp
+       p⊆exp : p ⊆ exp
+       q⊆exp : q ⊆ exp
 
 record ⊆-Ideal {L P : HOD } (LP : L ⊆ Power P) : Set (Level.suc n) where
    field
-       ideal : HOD   
-       i⊆L :  ideal ⊆ L 
+       ideal : HOD
+       i⊆L :  ideal ⊆ L
        ideal1 : { p q : HOD } →  L ∋ q  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
        exp : { p q : HOD } → ideal ∋ p → ideal ∋ q → Exp2 ideal p q
 
@@ -188,35 +188,35 @@
     ; generic = fdense
    } where
        ideal1 : {p q : HOD} → L ∋ q → PDHOD L p0 C ∋ p → q ⊆ p → PDHOD L p0 C ∋ q
-       ideal1 {p} {q} Lq record { gr = gr ; pn<gr = pn<gr ; x∈PP = x∈PP } q⊆p =  
+       ideal1 {p} {q} Lq record { gr = gr ; pn<gr = pn<gr ; x∈PP = x∈PP } q⊆p =
                  record { gr = gr ; pn<gr = λ y qy → pn<gr y (gf00 qy) ; x∈PP = Lq }  where
-            gf00 : {y : Ordinal } →  odef (* (& q)) y → odef (* (& p)) y  
+            gf00 : {y : Ordinal } →  odef (* (& q)) y → odef (* (& p)) y
             gf00 {y} qy = subst (λ k → odef k y ) (sym *iso) (q⊆p (subst (λ k → odef k y) *iso qy ))
        Lfp : (i : ℕ ) →  odef L (find-p L C i (& p0))
        Lfp zero = Lp0
        Lfp (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
        ... | yes y  = Lfp i
-       ... | no not  = proj1 ( ODC.x∋minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))) 
+       ... | no not  = proj1 ( ODC.x∋minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)))
        exp1 : {p q : HOD} → (ip : PDHOD L p0 C ∋ p) → (ip : PDHOD L p0 C ∋ q) → Exp2 (PDHOD L p0 C) p q
-       exp1 {p} {q} record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp } 
+       exp1 {p} {q} record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp }
                       record { gr = qgr ; pn<gr = qpn ; x∈PP = PPq } = gf01 where
-            Pp = record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp } 
-            Pq = record { gr = qgr ; pn<gr = qpn ; x∈PP = PPq } 
+            Pp = record { gr = pgr ; pn<gr = ppn ; x∈PP = PPp }
+            Pq = record { gr = qgr ; pn<gr = qpn ; x∈PP = PPq }
             gf17 : {q : HOD} → (Pq : PDHOD L p0 C ∋ q ) → PDHOD L p0 C ∋ * (find-p L C (gr Pq) (& p0))
-            gf17 {q} Pq = record { gr = PDN.gr Pq  ; pn<gr = λ y qq → subst (λ k → odef (* k) y) &iso qq  
-                 ; x∈PP = subst (λ k → odef L k ) (sym &iso) (Lfp (PDN.gr Pq))  } 
+            gf17 {q} Pq = record { gr = PDN.gr Pq  ; pn<gr = λ y qq → subst (λ k → odef (* k) y) &iso qq
+                 ; x∈PP = subst (λ k → odef L k ) (sym &iso) (Lfp (PDN.gr Pq))  }
             gf01 : Exp2 (PDHOD L p0 C) p q
             gf01 with <-cmp pgr qgr
-            ... | tri< a ¬b ¬c = record { exp = * (find-p L C (gr Pq) (& p0))  ; I∋exp = gf17 Pq ; p⊆exp = λ px → gf15 _ px 
+            ... | tri< a ¬b ¬c = record { exp = * (find-p L C (gr Pq) (& p0))  ; I∋exp = gf17 Pq ; p⊆exp = λ px → gf15 _ px
                     ; q⊆exp = λ {x} qx → qpn _ (subst (λ k → odef k x) (sym *iso) qx)  } where
                  gf16 : gr Pp ≤ gr Pq
                  gf16 = <to≤ a
                  gf15 :  (y : Ordinal) → odef p y → odef (* (find-p L C (gr Pq) (& p0))) y
                  gf15 y xpy = p-monotonic L p0 C gf16 (PDN.pn<gr Pp y (subst (λ k → odef k y) (sym *iso) xpy) )
             ... | tri≈ ¬a refl ¬c = record { exp = * (find-p L C (gr Pq) (& p0))  ; I∋exp = gf17 Pq
-                    ; p⊆exp = λ {x} px → ppn _ (subst (λ k → odef k x) (sym *iso) px)   
-                    ; q⊆exp = λ {x} qx → qpn _ (subst (λ k → odef k x) (sym *iso) qx)  } 
-            ... | tri> ¬a ¬b c = record { exp = * (find-p L C (gr Pp) (& p0))  ; I∋exp = gf17 Pp ; q⊆exp = λ qx → gf15 _ qx 
+                    ; p⊆exp = λ {x} px → ppn _ (subst (λ k → odef k x) (sym *iso) px)
+                    ; q⊆exp = λ {x} qx → qpn _ (subst (λ k → odef k x) (sym *iso) qx)  }
+            ... | tri> ¬a ¬b c = record { exp = * (find-p L C (gr Pp) (& p0))  ; I∋exp = gf17 Pp ; q⊆exp = λ qx → gf15 _ qx
                     ; p⊆exp = λ {x} px → ppn _ (subst (λ k → odef k x) (sym *iso) px)  } where
                  gf16 : gr Pq ≤ gr Pp
                  gf16 = <to≤ c
@@ -231,18 +231,18 @@
            fd09 (suc i) with is-o∅ ( & ( PGHOD i L C (find-p L C i (& p0))) )
            ... | yes _ = fd09 i
            ... | no not = fd17 where
-              fd19 =  ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))  
+              fd19 =  ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))
               fd18 : PGHOD i L C (find-p L C i (& p0)) ∋ fd19
               fd18 = ODC.x∋minimal O (PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq))
               fd17 :  odef L ( & (ODC.minimal O ( PGHOD i L C (find-p L C i (& p0))) (λ eq → not (=od∅→≡o∅ eq)))  )
-              fd17 = proj1 fd18 
+              fd17 = proj1 fd18
            an : ℕ
-           an = ctl← C (& (dense D)) MD  
+           an = ctl← C (& (dense D)) MD
            pn : Ordinal
            pn = find-p L C an (& p0)
            pn+1 : Ordinal
            pn+1 = find-p L C (suc an) (& p0)
-           d=an : dense D ≡ * (ctl→ C an) 
+           d=an : dense D ≡ * (ctl→ C an)
            d=an = begin dense D ≡⟨ sym *iso ⟩
                     * ( & (dense D)) ≡⟨ cong (*) (sym (ctl-iso→  C MD )) ⟩
                     * (ctl→ C an) ∎  where open ≡-Reasoning
@@ -267,11 +267,11 @@
               fd28 : PGHOD an L C (find-p L C an (& p0)) ∋ fd29
               fd28 = ODC.x∋minimal O (PGHOD an L C (find-p L C an (& p0))) (λ eq → not (=od∅→≡o∅ eq))
               fd27 :  odef (dense D) (& fd29)
-              fd27 = subst (λ k → odef k (& fd29)) (sym d=an) (proj1 (proj2 fd28)) 
+              fd27 = subst (λ k → odef k (& fd29)) (sym d=an) (proj1 (proj2 fd28))
            fd03 : odef (PDHOD L p0 C) pn+1
-           fd03 = record { gr = suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (suc an)} 
+           fd03 = record { gr = suc an ; pn<gr = λ y lt → lt ; x∈PP = fd09 (suc an)}
            fd01 : (dense D ∩ PDHOD L p0 C) ∋ (* pn+1)
-           fd01 = ⟪ subst (λ k → odef (dense D)  k ) (sym &iso) fd07 , subst (λ k → odef  (PDHOD L p0 C) k) (sym &iso) fd03 ⟫  
+           fd01 = ⟪ subst (λ k → odef (dense D)  k ) (sym &iso) fd07 , subst (λ k → odef  (PDHOD L p0 C) k) (sym &iso) fd03 ⟫
 
 open GenericFilter
 -- open Filter
@@ -281,42 +281,42 @@
       q r : HOD
       Lq : L ∋ q
       Lr : L ∋ r
-      p⊆q : p ⊆ q  
-      p⊆r : p ⊆ r  
+      p⊆q : p ⊆ q
+      p⊆r : p ⊆ r
       ¬compat : (s : HOD) → L ∋ s → ¬ ( (q ⊆ s) ∧ (r ⊆ s) )
 
 lemma232 : (P L p0 : HOD ) → (LPP : L ⊆ Power P) → (Lp0 : L ∋ p0 )
-      → (C : CountableModel ) 
+      → (C : CountableModel )
       → ctl-M C ∋ L
       → ( {p : HOD} → (Lp : L ∋ p ) → NotCompatible L p Lp )
       →  ¬ ( ctl-M C ∋  ⊆-Ideal.ideal (genf ( P-GenericFilter P L p0 LPP Lp0 C )))
-lemma232 P L p0 LPP Lp0 C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj1 rgf∩D) (proj2 rgf∩D)) 
+lemma232 P L p0 LPP Lp0 C ML NC MF = ¬rgf∩D=0 record { eq→ = λ {x} rgf∩D → ⊥-elim( proj2 (proj1 rgf∩D) (proj2 rgf∩D))
         ; eq← = λ lt → ⊥-elim (¬x<0 lt) } where
-    PG = P-GenericFilter P L p0 LPP Lp0 C 
+    PG = P-GenericFilter P L p0 LPP Lp0 C
     GF =  genf PG
     rgf =  ⊆-Ideal.ideal (genf PG)
     M = ctl-M C
-    D : HOD  
+    D : HOD
     D = L ＼ rgf
     D<M : & D o< & (ctl-M C)
     D<M = ordtrans≤-<  (⊆→o≤ proj1 ) (odef< ML)
     M∋DM : M ∋ (D ∩ M )
     M∋DM = is-model C D D<M
-    -- G⊆M : rgf ⊆ M  
+    -- G⊆M : rgf ⊆ M
     -- G⊆M {x} rx = TC C ML (subst (λ k → odef k x) (sym *iso) (⊆-Ideal.i⊆L GF rx))
     -- D⊆M : D ⊆ M
     -- D⊆M {x} dx = TC C ML (subst (λ k → odef k x) (sym *iso) (proj1 dx))
-    D=D∩M : D ≡ D ∩ M 
+    D=D∩M : D ≡ D ∩ M
     D=D∩M = ==→o≡ record { eq→ = ddm00 ; eq← = proj1 } where
         ddm00 : {x : Ordinal} → odef D x → odef (D ∩ M) x
         ddm00 {x} ⟪ Lx , ¬Gx ⟫ = ⟪ ⟪ Lx , ¬Gx  ⟫  , TC C ML (subst (λ k → odef k x) (sym *iso) Lx ) ⟫
-    M∋D : M ∋ D 
+    M∋D : M ∋ D
     M∋D = subst (λ k → M ∋ k ) (sym D=D∩M) M∋DM
     D⊆PP : D ⊆ Power P
-    D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx 
-    DD : Dense L 
+    D⊆PP {x} ⟪ Lx , ngx ⟫  = LPP Lx
+    DD : Dense L
     DD = record { dense = D ; d⊆P = proj1 ; has-exp = exp } where
-        exp : {p : HOD} → (Lp : L ∋ p) → Expansion p D 
+        exp : {p : HOD} → (Lp : L ∋ p) → Expansion p D
         exp {p} Lp = exp1 where
             q : HOD
             q = NotCompatible.q (NC Lp)
@@ -326,16 +326,16 @@
             Lq = NotCompatible.Lq (NC Lp)
             Lr : L ∋ r
             Lr = NotCompatible.Lr (NC Lp)
-            exp1 : Expansion p D 
+            exp1 : Expansion p D
             exp1  with ODC.p∨¬p O (rgf ∋ q)
-            ... | case2 ngq = record { exp = q  ; D∋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 { exp = r  ; D∋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 ( NotCompatible.¬compat (NC Lp) ex2 Le ⟪  q⊆ex2 , r⊆ex2 ⟫ ) where
                 ex2 = Exp2.exp (⊆-Ideal.exp GF gq gr)
                 Le =  ⊆-Ideal.i⊆L GF (Exp2.I∋exp (⊆-Ideal.exp GF gq gr))
-                q⊆ex2 = Exp2.p⊆exp (⊆-Ideal.exp GF gq gr) 
-                r⊆ex2 = Exp2.q⊆exp (⊆-Ideal.exp GF gq gr) 
+                q⊆ex2 = Exp2.p⊆exp (⊆-Ideal.exp GF gq gr)
+                r⊆ex2 = Exp2.q⊆exp (⊆-Ideal.exp GF gq gr)
     ¬rgf∩D=0 : ¬ ( (D ∩ rgf ) =h= od∅ )
     ¬rgf∩D=0 eq =  generic PG DD M∋D (==→o≡ eq)
 
@@ -357,10 +357,10 @@
     & (* y , * y) <⟨ c<→o< (v01 _ _)  ⟩
     & < * y , * p > <⟨ odef< xyp ⟩
     & (* x) ≡⟨ &iso ⟩
-    x ∎ ) where 
+    x ∎ ) where
        v00 : (x y : HOD) → odef (x , y) (& x)
        v00 _ _ = case1 refl
-       v01 : (x y : HOD) → < x , y > ∋ (x , x) 
+       v01 : (x y : HOD) → < x , y > ∋ (x , x)
        v01 _ _ = case1 refl
        open o≤-Reasoning O
 
@@ -380,9 +380,3 @@
   ind x valy = record { od = record { def = λ z → valS (⊆-Ideal.ideal (genf G)) x z  valy  } ; odmax = x ; <odmax = v02 } where
       v02 : {z : Ordinal} → valS (⊆-Ideal.ideal (genf G)) x z valy → z o< x
       v02 {z} lt = valS.z<x lt
-
-
-
-
-
-