### changeset 329:5544f4921a44

...
author Shinji KONO Sun, 05 Jul 2020 12:32:09 +0900 72f3e3b44c27 0faa7120e4b5 BAlgbra.agda ODC.agda OPair.agda Ordinals.agda filter.agda ordinal.agda 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) }```