# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1680406866 -32400
# Node ID 30540f151ae0fd59a3a330d050bb7c73fc8e4de7
# Parent  2a176e2694ab4cde83dcdda65be1d4871b7725ea
...

diff -r 2a176e2694ab -r 30540f151ae0 src/generic-filter.agda
--- a/src/generic-filter.agda	Wed Mar 29 10:25:46 2023 +0900
+++ b/src/generic-filter.agda	Sun Apr 02 12:41:06 2023 +0900
@@ -72,6 +72,27 @@
 
 -- we expect  P ∈ * ctl-M ∧ G  ⊆ L ⊆ Power P  , ¬ G ∈ * ctl-M,
 
+record COD : Set (Level.suc (Level.suc n)) where
+   field
+       CO : Ordinals {n}
+       CA : OD.ODAxiom CO
+       cod→ : ℕ → Ordinals.Ordinal CO
+       cod← : Ordinals.Ordinal CO → ℕ
+       cod-iso→ : { x : Ordinals.Ordinal CO } → cod→ (cod← x) ≡ x
+       cod-iso← : { x : ℕ } → cod← (cod→ x) ≡ x
+       -- Since it is countable, it is HOD.
+
+CM : COD → CountableModel 
+CM cod = record { 
+       ctl-M = ?
+     ; ctl→ = λ n → ?
+     ; ctl<M = λ n → ?
+     ; ctl← = λ x → ?
+     ; ctl-iso→ = ?
+     ; TC = ?
+     ; is-model = ?
+       }
+
 open CountableModel
 
 ----
@@ -392,7 +413,7 @@
        x∋gi : odef (* x) gi
 
 MgH : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
-MgH {L} {P} LP M G = record { od = record { def = λ x → odef M x ∧ Mg LP M G x } ; odmax = & M ; <odmax = odef∧<  }
+MgH {L} {P} LP M G = record { od = record { def = λ x → (x o< & M) ∧ Mg LP M G x } ; odmax = & M ; <odmax = proj1  }
 
 MG1 : {L P : HOD} (LP : L ⊆ Power P) (M : HOD) (G : GenericFilter {L} {P} LP M) → HOD
 MG1 {L} {P} LP M G = M ∪ Union (MgH LP M G)