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

changeset 1273:30540f151ae0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Apr 2023 12:41:06 +0900
parents 2a176e2694ab
children b15dd4438d50
files src/generic-filter.agda
diffstat 1 files changed, 22 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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)