# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1591957274 -32400
# Node ID ef93c56ad3115a1ecb36197dde0848d6a4b4cd67
# Parent  359402cc6c3dcff2ba777c00165cd6cf157485a8# Parent  5de8905a5a2b83d3a4a364fca1d881e450135cec
...

diff -r 5de8905a5a2b -r ef93c56ad311 OD.agda
--- a/OD.agda	Sun Jun 07 20:29:12 2020 +0900
+++ b/OD.agda	Fri Jun 12 19:21:14 2020 +0900
@@ -53,9 +53,19 @@
 eq← ( ⇔→==  {x} {y}  eq ) {z} m = proj2 eq m 
 
 -- next assumptions are our axiom
---  it defines a subset of OD, which is called HOD, usually defined as
+--  In classical Set Theory, HOD is used, as a subset of OD, 
 --     HOD = { x | TC x ⊆ OD }
---  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x
+--  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
+--  This is not possible because we don't have V yet.
+--  We simply assume V=OD here.
+--
+--  We also assumes ODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
+--  ODs have an ovbious maximum, but Ordinals are not. This means, od→ord is not an on-to mapping.
+--
+--  ==→o≡ is necessary to prove axiom of extensionality.
+--
+--  In classical Set Theory, sup is defined by Uion. Since we are working on constructive logic,
+--  we need explict assumption on sup.
 
 record ODAxiom : Set (suc n) where      
   -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
diff -r 5de8905a5a2b -r ef93c56ad311 filter.agda
--- a/filter.agda	Sun Jun 07 20:29:12 2020 +0900
+++ b/filter.agda	Fri Jun 12 19:21:14 2020 +0900
@@ -35,19 +35,27 @@
 
 record Filter  ( L : OD  ) : Set (suc n) where
    field
-       filter : OD
-       proper : ¬ ( filter ∋ od∅ )
-       inL :  filter ⊆ L 
+       filter : OD   
+       ¬f∋∅ : ¬ ( filter ∋ od∅ )
+       f∋L :  filter ∋ L
+       f⊆PL :  filter ⊆ Power L 
        filter1 : { p q : OD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
        filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
 
-open Filter
+record Ideal  ( L : OD  ) : Set (suc n) where
+   field
+       ideal : OD   
+       i∋∅ : ideal ∋ od∅ 
+       ¬i∋L : ¬ ( ideal ∋ L )
+       i⊆PL :  ideal ⊆ Power L 
+       ideal1 : { p q : OD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
+       ideal2 : { p q : OD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
 
-L⊆L : (L : OD) → L ⊆ L
-L⊆L L = record { incl = λ {x} lt → lt }
+open Filter
+open Ideal
 
 L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
-L-filter {L} P {p} lt = filter1 P {p} {L} (L⊆L L) lt {!!}
+L-filter {L} P {p} lt = {!!} -- filter1 P {p} {L} {!!} lt {!!}
 
 prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
 prime-filter {L} P {p} {q} =  filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
@@ -65,8 +73,7 @@
 
 generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
 generated-filter {L} P p = record {
-     proper = {!!} ; 
-     filter = {!!}  ; inL = {!!} ; 
+     filter = {!!}  ; 
      filter1 = {!!} ; filter2 = {!!}
    }
 
@@ -86,7 +93,7 @@
    import ordinal
 
    -- open  ordinal.C-Ordinal-with-choice 
-   -- both Power and infinite is too ZF, it is better to use simpler one
+
    Hω2 : Filter (Power (Power infinite))
    Hω2 = {!!}