--- a/src/generic-filter.agda	Mon Jan 23 10:20:55 2023 +0900
+++ b/src/generic-filter.agda	Sat Feb 18 11:51:22 2023 +0900
@@ -61,7 +61,8 @@
        ctl<M : (x : Nat) → odef (ctl-M) (ctl→ x) 
        ctl← : (x : Ordinal )→  odef (ctl-M ) x → Nat
        ctl-iso→ : { x : Ordinal } → (lt : odef (ctl-M) x )  → ctl→ (ctl← x lt ) ≡ x 
-       ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (ctl<M x)  ≡ x
+       -- we have no otherway round
+       -- ctl-iso← : { x : Nat }  →  ctl← (ctl→ x ) (ctl<M x)  ≡ x
 --
 -- almmost universe
 -- find-p contains ∃ x : Ordinal → x o< & M → ∀ r ∈ M → ∈ Ord x
@@ -241,6 +242,14 @@
     D = ?
 
 --
+-- P-Generic Filter defines a countable model D ⊂ C from P
+--
+
+--
+-- in D, we have V ≠ L
+--
+
+--
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
 --