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

changeset 329:5544f4921a44

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, 05 Jul 2020 12:32:09 +0900
parents 72f3e3b44c27
children 0faa7120e4b5
files BAlgbra.agda ODC.agda OPair.agda Ordinals.agda filter.agda ordinal.agda
diffstat 6 files changed, 124 insertions(+), 97 deletions(-) [+]
line wrap: on
line diff
--- a/BAlgbra.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/BAlgbra.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -24,16 +24,16 @@
 open _∨_
 open Bool
 
-_∩_ : ( A B : OD  ) → OD
+_∩_ : ( A B : HOD  ) → HOD
 A ∩ B = record { def = λ x → def A x ∧ def B x } 
 
-_∪_ : ( A B : OD  ) → OD
+_∪_ : ( A B : HOD  ) → HOD
 A ∪ B = record { def = λ x → def A x ∨ def B x } 
 
-_＼_ : ( A B : OD  ) → OD
+_＼_ : ( A B : HOD  ) → HOD
 A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
 
-∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B )
+∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
 ∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
     lemma1 :  {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x
     lemma1 {x} lt = lemma3 lt where
@@ -49,7 +49,7 @@
     lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
        (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x}))
 
-∩-Select : { A B : OD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
+∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
 ∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
     lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x
     lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) }
@@ -57,7 +57,7 @@
     lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
         record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } }
 
-dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
+dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
     lemma1 :  {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x
     lemma1 {x} lt with proj2 lt
@@ -67,7 +67,7 @@
     lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } 
     lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } 
 
-dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
+dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
     lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x
     lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
--- a/ODC.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/ODC.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -21,13 +21,18 @@
 open OD._==_
 open ODAxiom odAxiom
 
+open HOD
+
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
 postulate      
   -- mimimul and x∋minimal is an Axiom of choice
-  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD 
-  -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
-  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
+  -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
+  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
   -- minimality (may proved by ε-induction )
-  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
 
 
 --
@@ -35,23 +40,26 @@
 --     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
 --
 
-ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
-ppp  {p} {a} d = d
+-- ppp :  { p : Set n } { a : HOD  } → record { def = λ x → p } ∋ a → p
+-- ppp  {p} {a} d = d
 
-p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
-p∨¬p  p with is-o∅ ( od→ord ( record { def = λ x → p } ))
-p∨¬p  p | yes eq = case2 (¬p eq) where
-   ps = record { def = λ x → p }
-   lemma : ps == od∅ → p → ⊥
-   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq p0 )
-   ¬p : (od→ord ps ≡ o∅) → p → ⊥
-   ¬p eq = lemma ( subst₂ (λ j k → j ==  k ) oiso o∅≡od∅ ( o≡→== eq ))
-p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
-   ps = record { def = λ x → p }
-   eqo∅ : ps ==  od∅  → od→ord ps ≡  o∅  
-   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
-   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
-   lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
+-- p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
+-- p∨¬p  p with is-o∅ ( od→ord ( record { odef = λ x → p } ))
+-- p∨¬p  p | yes eq = case2 (¬p eq) where
+--    ps = record { odef = λ x → p }
+--    lemma : ps =h= od∅ → p → ⊥
+--    lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq p0 )
+--    ¬p : (od→ord ps ≡ o∅) → p → ⊥
+--    ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) oiso o∅≡od∅ ( o≡→== eq ))
+-- p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
+--    ps = record { odef = λ x → p }
+--    eqo∅ : ps =h=  od∅  → od→ord ps ≡  o∅  
+--    eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
+--    lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
+--    lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
+
+postulate 
+   p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
 
 decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
 decp  p with p∨¬p p
@@ -63,7 +71,7 @@
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
-OrdP : ( x : Ordinal  ) ( y : OD  ) → Dec ( Ord x ∋ y )
+OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
 OrdP  x y with trio< x (od→ord y)
 OrdP  x y | tri< a ¬b ¬c = no ¬c
 OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
@@ -71,26 +79,26 @@
 
 open import zfc
 
-OD→ZFC : ZFC
-OD→ZFC   = record { 
-    ZFSet = OD 
+HOD→ZFC : ZFC
+HOD→ZFC   = record { 
+    ZFSet = HOD 
     ; _∋_ = _∋_ 
-    ; _≈_ = _==_ 
+    ; _≈_ = _=h=_ 
     ; ∅  = od∅
     ; Select = Select
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select 
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select 
     isZFC = record {
        choice-func = choice-func ;
        choice = choice
      } where
          -- Axiom of choice ( is equivalent to the existence of minimal in our case )
          -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
-         choice-func : (X : OD  ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
+         choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
          choice-func X {x} not X∋x = minimal x not
-         choice : (X : OD  ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
+         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimal A not
 
--- a/OPair.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/OPair.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -17,6 +17,7 @@
 open inOrdinal O
 open OD O
 open OD.OD
+open OD.HOD
 open ODAxiom odAxiom
 
 open _∧_
@@ -25,30 +26,33 @@
 
 open _==_
 
-<_,_> : (x y : OD) → OD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
+<_,_> : (x y : HOD) → HOD
 < x , y > = (x , x ) , (x , y )
 
-exg-pair : { x y : OD } → (x , y ) == ( y , x )
+exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
-    left : {z : Ordinal} → def (x , y) z → def (y , x) z 
+    left : {z : Ordinal} → odef (x , y) z → odef (y , x) z 
     left (case1 t) = case2 t
     left (case2 t) = case1 t
-    right : {z : Ordinal} → def (y , x) z → def (x , y) z 
+    right : {z : Ordinal} → odef (y , x) z → odef (x , y) z 
     right (case1 t) = case2 t
     right (case2 t) = case1 t
 
-ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
+ord≡→≡ : { x y : HOD } → od→ord x ≡ od→ord y → x ≡ y
 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
 
 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
 
-eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
 eq-prod refl refl = refl
 
-prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
-    lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
+    lemma0 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
     lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) 
     lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
     lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
@@ -57,15 +61,15 @@
     lemma0 {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
     lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
     lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
-    lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
+    lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
     lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
-        lemma3 : ( x , x ) == ( y , z )
+        lemma3 : ( x , x ) =h= ( y , z )
         lemma3 = ==-trans eq exg-pair
-    lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
+    lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
     lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
     lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
     lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
-    lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
+    lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
     lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
     lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
     ... | refl with lemma2 (==-sym eq )
@@ -81,6 +85,9 @@
     ... | refl with lemma4 eq -- with (x,y)≡(x,y')
     ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
 
+--
+-- unlike ordered pair, ZFProduct is not a HOD
+
 data ord-pair : (p : Ordinal) → Set n where
    pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
 
@@ -94,35 +101,38 @@
 pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
 pi1 ( pair x y) = x
 
-π1 : { p : OD } → ZFProduct ∋ p → OD
+π1 : { p : HOD } → def ZFProduct (od→ord p) → HOD
 π1 lt = ord→od (pi1 lt )
 
 pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
 pi2 ( pair x y ) = y
 
-π2 : { p : OD } → ZFProduct ∋ p → OD
+π2 : { p : HOD } → def ZFProduct (od→ord p) → HOD
 π2 lt = ord→od (pi2 lt )
 
-op-cons :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >  
+op-cons :  { ox oy  : Ordinal } → def ZFProduct (od→ord ( < ord→od ox , ord→od oy >   ))
 op-cons {ox} {oy} = pair ox oy
 
-p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
-p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
-    let open ≡-Reasoning in begin
-        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
-    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
-        od→ord < x , y >
-    ∎ ) 
+def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
+def-subst df refl refl = df
+
+p-cons :  ( x y  : HOD ) → def ZFProduct (od→ord ( < x , y >))
+p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
+   let open ≡-Reasoning in begin
+       od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
+   ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
+       od→ord < x , y >
+   ∎ ) 
 
 op-iso :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
 op-iso (pair ox oy) = refl
 
-p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x
+p-iso :  { x  : HOD } → (p : def ZFProduct (od→ord  x) ) → < π1 p , π2 p > ≡ x
 p-iso {x} p = ord≡→≡ (op-iso p) 
 
-p-pi1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π1 p ≡ x
+p-pi1 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π1 p ≡ x
 p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
 
-p-pi2 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π2 p ≡ y
+p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
--- a/Ordinals.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/Ordinals.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -20,7 +20,7 @@
      ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
-     is-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → x ≡ osuc y) )
+     not-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
      next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y )
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
--- a/filter.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/filter.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -29,45 +29,45 @@
 open Bool
 
 -- Kunen p.76 and p.53, we use ⊆
-record Filter  ( L : OD  ) : Set (suc n) where
+record Filter  ( L : HOD  ) : Set (suc n) where
    field
-       filter : OD   
+       filter : HOD   
        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)
+       filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
 
 open Filter
 
-record prime-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
+record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
    field
        proper  : ¬ (filter P ∋ od∅)
-       prime   : {p q : OD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+       prime   : {p q : HOD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
 
-record ultra-filter { L : OD } (P : Filter L) : Set (suc (suc n)) where
+record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
    field
        proper  : ¬ (filter P ∋ od∅)
-       ultra   : {p : OD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
+       ultra   : {p : HOD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
 
 open _⊆_
 
-trans-⊆ :  { A B C : OD} → A ⊆ B → B ⊆ C → A ⊆ C
+trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
 
-power→⊆ :  ( A t : OD) → Power A ∋ t → t ⊆ A
-power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
-   t1 : {x : OD }  → t ∋ x → ¬ ¬ (A ∋ x)
+power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
+power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → HODC.double-neg-eilm O (t1 t∋x) } where
+   t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
    t1 = zf.IsZF.power→ isZF A t PA∋t
 
-∈-filter : {L p : OD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
+∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
 ∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
 
-∪-lemma1 : {L p q : OD } → (p ∪ q)  ⊆ L → p ⊆ L
+∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
 ∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
 
-∪-lemma2 : {L p q : OD } → (p ∪ q)  ⊆ L → q ⊆ L
+∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
 ∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
 
-q∩q⊆q : {p q : OD } → (q ∩ p) ⊆ q 
+q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
 -----
@@ -75,12 +75,12 @@
 --  ultra filter is prime
 --
 
-filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ultra-filter P  → prime-filter P 
+filter-lemma1 :  {L : HOD} → (P : Filter L)  → ∀ {p q : HOD } → ultra-filter P  → prime-filter P 
 filter-lemma1 {L} P u = record {
          proper = ultra-filter.proper u
        ; prime = lemma3
     } where
-  lemma3 : {p q : OD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+  lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
   lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
   ... | case1 p∈P  = case1 p∈P
   ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
@@ -104,28 +104,28 @@
 --  if Filter contains L, prime filter is ultra
 --
 
-filter-lemma2 :  {L : OD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
+filter-lemma2 :  {L : HOD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
 filter-lemma2 {L} P f∋L prime = record {
          proper = prime-filter.proper prime
        ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
    } where
         open _==_
-        p+1-p=1 : {p : OD} → p ⊆ L → L == (p ∪ (L ＼ p)) 
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (def p x)
+        p+1-p=1 : {p : HOD} → p ⊆ L → L == (p ∪ (L ＼ p)) 
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt with HODC.decp O (def p x)
         eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
         eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
         eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → def L k ) diso (incl p⊆L ( subst (λ k → def p k) (sym diso) p∋x  )) 
         eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
-        lemma : (p : OD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
+        lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
         lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L
 
-record Dense  (P : OD ) : Set (suc n) where
+record Dense  (P : HOD ) : Set (suc n) where
    field
-       dense : OD
+       dense : HOD
        incl :  dense ⊆ P 
-       dense-f : OD → OD
-       dense-d :  { p : OD} → P ∋ p  → dense ∋ dense-f p  
-       dense-p :  { p : OD} → P ∋ p  →  p ⊆ (dense-f p) 
+       dense-f : HOD → HOD
+       dense-d :  { p : HOD} → P ∋ p  → dense ∋ dense-f p  
+       dense-p :  { p : HOD} → P ∋ p  →  p ⊆ (dense-f p) 
 
 --    the set of finite partial functions from ω to 2
 --
@@ -134,18 +134,18 @@
 --
 -- Hω2 : Filter (Power (Power infinite))
 
-record Ideal  ( L : OD  ) : Set (suc n) where
+record Ideal  ( L : HOD  ) : Set (suc n) where
    field
-       ideal : OD   
+       ideal : HOD   
        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)
+       ideal1 : { p q : HOD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
+       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
 
 open Ideal
 
-proper-ideal : {L : OD} → (P : Ideal L ) → {p : OD} → Set n
+proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
 proper-ideal {L} P {p} = ideal P ∋ od∅
 
-prime-ideal : {L : OD} → Ideal L → ∀ {p q : OD } → Set n
+prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
 prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
 
--- a/ordinal.agda	Sun Jul 05 11:40:55 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 12:32:09 2020 +0900
@@ -211,7 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
-   ; next = {!!}
+   ; next = next
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -219,10 +219,19 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
-     ; is-limit = {!!}
-     ; next-limit = {!!}
+     ; not-limit = not-limit
+     ; next-limit = next-limit
    }
   } where
+     next : Ordinal {suc n} → Ordinal {suc n}
+     next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
+     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y)
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
+         lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
+         lemma x (case1 lt) = case1 lt
+     not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
+     not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
+     not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
      TransFinite1 : { ψ : ord1  → Set (suc n) }