### changeset 256:6e1c60866788release

orderd pair and product
author Shinji KONO Thu, 29 Aug 2019 16:18:37 +0900 fe8392f527eb (current diff) 1eba96b7ab8d (diff) 4fcac1eebc74 7 files changed, 264 insertions(+), 152 deletions(-) [+]
line wrap: on
line diff
```--- a/.hgtags	Mon Aug 12 09:04:16 2019 +0900
+++ b/.hgtags	Thu Aug 29 16:18:37 2019 +0900
@@ -13,3 +13,5 @@
2c7d45734e3be59a06d272a07fecdbf77ab8ce10 current
2c7d45734e3be59a06d272a07fecdbf77ab8ce10 current
1b1620e2053cfc340a4df0d63de65b9059b19b6f current
+1b1620e2053cfc340a4df0d63de65b9059b19b6f current
+2ea2a19f9cd638b29af51a47fa3dabdaea381d5c current```
```--- a/OD.agda	Mon Aug 12 09:04:16 2019 +0900
+++ b/OD.agda	Thu Aug 29 16:18:37 2019 +0900
@@ -33,7 +33,7 @@
eq→ : ∀ { x : Ordinal  } → def a x → def b x
eq← : ∀ { x : Ordinal  } → def b x → def a x

-id : {n : Level} {A : Set n} → A → A
+id : {A : Set n} → A → A
id x = x

eq-refl :  {  x :  OD  } → x == x
@@ -171,6 +171,70 @@
is-o∅ x | tri≈ ¬a b ¬c = yes b
is-o∅ x | tri> ¬a ¬b c = no ¬b

+_,_ : OD  → OD  → OD
+x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } --  Ord (omax (od→ord x) (od→ord y))
+<_,_> : (x y : OD) → OD
+< x , y > = (x , x ) , (x , y )
+
+exg-pair : { x y : OD } → (x , y ) == ( y , x )
+exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
+    left : {z : Ordinal} → def (x , y) z → def (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 (case1 t) = case2 t
+    right (case2 t) = case1 t
+
+==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
+==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }
+
+==-sym : { x y  : OD } →  x == y →  y == x
+==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← =  λ {m} t → eq→ x=y t }
+
+ord≡→≡ : { x y : OD } → 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 refl refl = refl
+
+prod-eq : { x x' y y' : OD } → < x , y > == < 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} 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 )
+    lemma0 {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
+    lemma0 {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
+    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} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
+        lemma3 : ( x , x ) == ( y , z )
+        lemma3 = ==-trans eq exg-pair
+    lemma1 : {x y : OD } → ( x , x ) == ( 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} 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 )
+    ... | refl = refl
+    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
+    lemmax : x ≡ x'
+    lemmax with eq→ eq {od→ord (x , x)} (case1 refl)
+    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
+    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
+    ... | refl = lemma1 (ord→== s )
+    lemmay : y ≡ y'
+    lemmay with lemmax
+    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
+    ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
+
ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
ppp  {p} {a} d = d

@@ -193,13 +257,13 @@
lemma : ps ∋ minimul ps (λ eq →  ¬p (eqo∅ eq))
lemma = x∋minimul ps (λ eq →  ¬p (eqo∅ eq))

-∋-p : ( p : Set n ) → Dec p   -- assuming axiom of choice
-∋-p  p with p∨¬p p
-∋-p  p | case1 x = yes x
-∋-p  p | case2 x = no x
+decp : ( p : Set n ) → Dec p   -- assuming axiom of choice
+decp  p with p∨¬p p
+decp  p | case1 x = yes x
+decp  p | case2 x = no x

double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm  {A} notnot with ∋-p  A                         -- assuming axiom of choice
+double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
... | yes p = p
... | no ¬p = ⊥-elim ( notnot ¬p )

@@ -268,8 +332,6 @@
Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
Replace : OD  → (OD  → OD  ) → OD
Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
-    _,_ : OD  → OD  → OD
-    x , y = Ord (omax (od→ord x) (od→ord y))
_∩_ : ( A B : ZFSet  ) → ZFSet
A ∩ B = record { def = λ x → def A x ∧ def B x }
Union : OD  → OD
@@ -294,7 +356,8 @@
isZF : IsZF (OD )  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
isZF = record {
isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
-       ;   pair  = pair
+       ;   pair→  = pair→
+       ;   pair←  = pair←
;   union→ = union→
;   union← = union←
;   empty = empty
@@ -311,9 +374,17 @@
;   choice = choice
} where

-         pair : (A B : OD  ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
-         proj1 (pair A B ) = omax-x  (od→ord A) (od→ord B)
-         proj2 (pair A B ) = omax-y  (od→ord A) (od→ord B)
+         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y )
+         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x ))
+         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y ))
+
+         pair← : ( x y t : ZFSet  ) → ( t == x ) ∨ ( t == y ) →  (x , y)  ∋ t
+         pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
+         pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y))
+
+         -- pair0 : (A B : OD  ) → ((A , B) ∋ A) ∧  ((A , B) ∋ B)
+         -- proj1 (pair A B ) = omax-x  (od→ord A) (od→ord B)
+         -- proj2 (pair A B ) = omax-y  (od→ord A) (od→ord B)

empty : (x : OD  ) → ¬  (od∅ ∋ x)
empty x = ¬x<0
@@ -477,10 +548,55 @@
choice : (X : OD  ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
choice X {A} X∋A not = x∋minimul A not

-_,_ = ZF._,_ OD→ZF
+         ---
+         --- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+         ---
+         record choiced  ( X : OD) : Set (suc n) where
+          field
+             a-choice : OD
+             is-in : X ∋ a-choice
+
+         choice-func' :  (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
+         choice-func'  X p∨¬p not = have_to_find where
+                 ψ : ( ox : Ordinal ) → Set (suc n)
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
+                 lemma-ord : ( ox : Ordinal  ) → ψ ox
+                 lemma-ord  ox = TransFinite {ψ} induction ox where
+                    ∋-p : (A x : OD ) → Dec ( A ∋ x )
+                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x ))
+                    ∋-p A x | case1 (lift t)  = yes t
+                    ∋-p A x | case2 t  = no (λ x → t (lift x ))
+                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set (suc n) }
+                        → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
+                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x))
+                    ∀-imply-or  {A} {B} ∀AB | case1 (lift t) = case1 t
+                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x (lift not ))) where
+                         lemma : ¬ ((x : Ordinal ) → A x) →  B
+                         lemma not with p∨¬p B
+                         lemma not | case1 b = b
+                         lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
+                    induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
+                    induction x prev with ∋-p X ( ord→od x)
+                    ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
+                    ... | no ¬p = lemma where
+                         lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
+                         lemma1 y with ∋-p X (ord→od y)
+                         lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
+                         lemma = ∀-imply-or lemma1
+                 have_to_find : choiced X
+                 have_to_find with lemma-ord (od→ord X )
+                 have_to_find | t = dont-or  t ¬¬X∋x where
+                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
+                     ¬¬X∋x nn = not record {
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt)
+                          ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
+                        }
+
+
Union = ZF.Union OD→ZF
Power = ZF.Power OD→ZF
Select = ZF.Select OD→ZF
Replace = ZF.Replace OD→ZF
isZF = ZF.isZF  OD→ZF
-TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)```
```--- a/Ordinals.agda	Mon Aug 12 09:04:16 2019 +0900
+++ b/Ordinals.agda	Thu Aug 29 16:18:37 2019 +0900
@@ -50,6 +50,7 @@
¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
<-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
+        TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)

o<-dom :   { x y : Ordinal } → x o< y → Ordinal
o<-dom  {x} _ = x```
```--- a/cardinal.agda	Mon Aug 12 09:04:16 2019 +0900
+++ b/cardinal.agda	Thu Aug 29 16:18:37 2019 +0900
@@ -20,40 +20,106 @@
open _∧_
open _∨_
open Bool
+open _==_

-- we have to work on Ordinal to keep OD Level n
-- since we use p∨¬p which works only on Level n
+--   < x , y > = (x , x) , (x , y)
+
+data ord-pair : (p : Ordinal) → Set n where
+   pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
+
+ZFProduct : OD
+ZFProduct = record { def = λ x → ord-pair x }
+
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
+-- eq-pair refl refl = HE.refl
+
+pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi1 ( pair x y) = x
+
+π1 : { p : OD } → ZFProduct ∋ p → Ordinal
+π1 lt = pi1 lt
+
+pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi2 ( pair x y ) = y
+
+π2 : { p : OD } → ZFProduct ∋ p → Ordinal
+π2 lt = pi2 lt
+
+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 >
+    ∎ )
+
+
+p-iso1 :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
+p-iso1 {ox} {oy} = pair ox oy
+
+p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
+p-iso {x} p = ord≡→≡ (lemma p) where
+    lemma :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
+    lemma (pair ox oy) = refl
+
+
+∋-p : (A x : OD ) → Dec ( A ∋ x )
+∋-p A x with p∨¬p ( A ∋ x )
+∋-p A x | case1 t = yes t
+∋-p A x | case2 t = no t
+
+_⊗_  : (A B : OD) → OD
+A ⊗ B  = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where
+    checkAB : { p : Ordinal } → def ZFProduct p → Set n
+    checkAB (pair x y) = def A x ∧ def B y
+
+func→od0  : (f : Ordinal → Ordinal ) → OD
+func→od0  f = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) } where
+    checkfunc : { p : Ordinal } → def ZFProduct p → Set n
+    checkfunc (pair x y) = f x ≡ y
+
+--  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
+
+Func :  ( A B : OD ) → OD
+Func A B = record { def = λ x → def (Power (A ⊗ B)) x }
+
+-- power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+

func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
-func→od f dom = Replace dom ( λ x →  x , (ord→od (f (od→ord x) )))
-
-record _⊗_  (A B : Ordinal) : Set n where
-   field
-      π1 : Ordinal
-      π2 : Ordinal
-      A∋π1 : def (ord→od A)  π1
-      B∋π2 : def (ord→od B)  π2
+func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )

--- Clearly wrong. We need ordered pair
-Func :  ( A B : OD ) → OD
-Func A B = record { def = λ x → (od→ord A) ⊗ (od→ord B) }
-
-open  _⊗_
+record Func←cd { dom cod : OD } {f : Ordinal }  : Set n where
+   field
+      func-1 : Ordinal → Ordinal
+      func→od∈Func-1 :  Func dom cod ∋  func→od func-1 dom
+
+od→func : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f  → Func←cd {dom} {cod} {f}
+od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
+   lemma : Ordinal → Ordinal → Ordinal
+   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma x y | p | no n  = o∅
+   lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y)
+           lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
+           lemma2 (pair x1 y1) with decp ( x1 ≡ x)
+           lemma2 (pair x1 y1) | yes p = y1
+           lemma2 (pair x1 y1) | no ¬p = o∅
+   fod : OD
+   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > )

-func←od : { dom cod : OD } → (f : OD )  → Func dom cod ∋ f → (Ordinal → Ordinal )
-func←od {dom} {cod} f lt x = sup-o ( λ y → lemma  y ) where
-   lemma : Ordinal → Ordinal
-   lemma y with p∨¬p ( _⊗_.π1 lt ≡ x )
-   lemma y | case1 refl = _⊗_.π2 lt
-   lemma y | case2 not = o∅
+
+open Func←cd

-- contra position of sup-o<
--

-postulate
-  -- contra-position of mimimulity of supermum required in Cardinal
-  sup-x  : ( Ordinal  → Ordinal ) →  Ordinal
-  sup-lb : { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
+-- postulate
+--   -- contra-position of mimimulity of supermum required in Cardinal
+--   sup-x  : ( Ordinal  → Ordinal ) →  Ordinal
+--   sup-lb : { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))

------------
--
@@ -68,7 +134,8 @@
ymap : Ordinal
xfunc : def (Func X Y) xmap
yfunc : def (Func Y X) ymap
-       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → func←od (ord→od xmap) xfunc ( func←od (ord→od ymap) yfunc y )  ≡ y
+       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) →
+          func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func  yfunc) y )  ≡ y

open Onto

@@ -88,7 +155,7 @@
xfunc1 = {!!}
zfunc : def (Func Z X) zmap
zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od (ord→od xmap1) xfunc1 ( func←od (ord→od zmap) zfunc z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func-1 (od→func  xfunc1 )  (func-1 (od→func  zfunc ) z )  ≡ z
onto-iso1   = {!!}

```
```--- a/filter.agda	Mon Aug 12 09:04:16 2019 +0900
+++ b/filter.agda	Thu Aug 29 16:18:37 2019 +0900
@@ -1,8 +1,10 @@
open import Level
-open import OD
+open import Ordinals
+module filter {n : Level } (O : Ordinals {n})   where
+
open import zf
-open import ordinal
-module filter ( n : Level )  where
+open import logic
+import OD

open import Relation.Nullary
open import Relation.Binary
@@ -12,23 +14,28 @@
open import  Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )

-od = OD→ZF {n}
-
+open inOrdinal O
+open OD O
+open OD.OD

-record Filter {n : Level} ( P max : OD {suc n} )  : Set (suc (suc n)) where
+open _∧_
+open _∨_
+open Bool
+
+record Filter  ( P max : OD  )  : Set (suc n) where
field
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
-       G : OD {suc n}
+       _⊇_ : OD  → OD  → Set n
+       G : OD
G∋1 : G ∋ max
-       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  max
-       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
-       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
-           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+       Gmax : { p : OD  } → P ∋ p → p ⊇  max
+       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))

-dense :  {n : Level} → Set (suc (suc n))
-dense {n} = { D P p : OD {suc n} } → ({x : OD {suc n}} → P ∋ p → ¬ ( ( q : OD {suc n}) → D ∋ q → od→ord p o< od→ord q ))
+dense :   Set (suc n)
+dense = { D P p : OD  } → ({x : OD } → P ∋ p → ¬ ( ( q : OD ) → D ∋ q → od→ord p o< od→ord q ))

-record NatFilter {n : Level} ( P : Nat → Set n)  : Set (suc n) where
+record NatFilter  ( P : Nat → Set n)  : Set (suc n) where
field
GN : Nat → Set n
GN∋1 : GN 0
@@ -46,16 +53,16 @@

-- H(ω,2) = Power ( Power ω ) = Def ( Def ω))

-Pred : {n : Level} ( Dom : OD {suc n} ) → OD {suc n}
-Pred {n} dom = record {
-      def = λ x → def dom x → Set n
+Pred :  ( Dom : OD  ) → OD
+Pred  dom = record {
+      def = λ x → def dom x → {!!}
}

-Hω2 : {n : Level} →  OD {suc n}
-Hω2 {n} = record { def = λ x → {dom : Ordinal {suc n}} → x ≡ od→ord ( Pred ( ord→od dom )) }
+Hω2 :   OD
+Hω2  = record { def = λ x → {dom : Ordinal } → x ≡ od→ord ( Pred ( ord→od dom )) }

-Hω2Filter :   {n : Level} → Filter {n} Hω2 od∅
-Hω2Filter {n} = record {
+Hω2Filter :     Filter  Hω2 od∅
+Hω2Filter  = record {
_⊇_ = _⊇_
; G = {!!}
; G∋1 = {!!}
@@ -64,17 +71,17 @@
; Gcompat = {!!}
} where
P = Hω2
-       _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)
+       _⊇_ : OD  → OD  → Set n
_⊇_ = {!!}
-       G : OD {suc n}
+       G : OD
G = {!!}
G∋1 : G ∋ od∅
G∋1 = {!!}
-       Gmax : { p : OD {suc n} } → P ∋ p → p ⊇  od∅
+       Gmax : { p : OD  } → P ∋ p → p ⊇  od∅
Gmax = {!!}
-       Gless : { p q : OD {suc n} } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
+       Gless : { p q : OD  } → G ∋ p → P ∋ q →  p ⊇ q  → G ∋ q
Gless = {!!}
-       Gcompat : { p q : OD {suc n} } → G ∋ p → G ∋ q → ¬ (
-           ( r : OD {suc n}) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
+       Gcompat : { p q : OD  } → G ∋ p → G ∋ q → ¬ (
+           ( r : OD ) →  ((  p ⊇  r ) ∧ (  p ⊇ r )))
Gcompat = {!!}
```
```--- a/ordinal.agda	Mon Aug 12 09:04:16 2019 +0900
+++ b/ordinal.agda	Thu Aug 29 16:18:37 2019 +0900
@@ -1,4 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
open import Level
module ordinal where

@@ -204,21 +203,6 @@
lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )
lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1

--- we cannot prove this in intutionistic logic
---  (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p )  → p
--- postulate
---  TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
---   → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
---   → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → p )
---   → p
---
---
-TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
-  → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → ¬ p )
-  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
-  → ¬ p
-TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )

open import Ordinals

@@ -322,69 +306,3 @@
dz<dz  : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x
dz<dz refl = s<refl

-  ---
-  --- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
-  ---
-  record choiced  ( X : OD) : Set (suc (suc n)) where
-   field
-      a-choice : OD
-      is-in : X ∋ a-choice
-
-  choice-func' :  (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
-  choice-func'  X p∨¬p not = have_to_find where
-          ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
-          ψ ox = (( x : Ordinal {suc n}) → x o< ox  → ( ¬ def X x )) ∨ choiced X
-          lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
-          lemma-ord  ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where
-             ∋-p' : (A x : OD ) → Dec ( A ∋ x )
-             ∋-p' A x with p∨¬p ( A ∋ x )
-             ∋-p' A x | case1 t = yes t
-             ∋-p' A x | case2 t = no t
-             ∀-imply-or :  {n : Level}  {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
-                 → ((x : Ordinal {suc n}) → A x ∨ B) →  ((x : Ordinal {suc n}) → A x) ∨ B
-             ∀-imply-or {n} {A} {B} ∀AB with p∨¬p  ((x : Ordinal {suc n}) → A x)
-             ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
-             ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
-                  lemma : ¬ ((x : Ordinal {suc n}) → A x) →  B
-                  lemma not with p∨¬p B
-                  lemma not | case1 b = b
-                  lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
-             caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
-             caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
-             caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
-             caseΦ lx prev | no ¬p = lemma where
-                  lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
-                  lemma1 x with trio< x (ordinal lx (Φ lx))
-                  lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
-                      lemma2 : x o< (ordinal lx (Φ lx)) →  osuc x o< ordinal lx (Φ lx)
-                      lemma2 (case1 lt) = case1 lt
-                  lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
-                  lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
-                  lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
-                  lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
-                  lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
-                  lemma = ∀-imply-or lemma1
-             caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
-             caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
-             caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
-             caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
-                  lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
-                  lemma y lt with trio< y (ordinal lx x )
-                  lemma y lt | tri< a ¬b ¬c = not_found y a
-                  lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
-                  lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
-                  lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
-                  lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
-             caseOSuc lx x (case2 found) | no ¬p = case2 found
-             caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) →
-                 ψ (record { lv = lx ; ord = OSuc lx x })
-             caseOSuc1 lx x lt =  caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl))
-          have_to_find : choiced X
-          have_to_find with lemma-ord (od→ord X )
-          have_to_find | t = dont-or  t ¬¬X∋x where
-              ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥)
-              ¬¬X∋x nn = not record {
-                     eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt)
-                   ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
-                 }
-  ```
```--- a/zf.agda	Mon Aug 12 09:04:16 2019 +0900
+++ b/zf.agda	Thu Aug 29 16:18:37 2019 +0900
@@ -22,8 +22,9 @@
: Set (suc (n ⊔ m)) where
field
isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_
-     -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
-     pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
+     -- ∀ x ∀ y ∃ z ∀ t ( z ∋ t → t ≈ x ∨ t  ≈ y)
+     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y )
+     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t
-- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
@@ -34,7 +35,7 @@
_∩_ : ( A B : ZFSet  ) → ZFSet
A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
_∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easer
+  A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easier
｛_｝ : ZFSet → ZFSet
｛ x ｝ = ( x ,  x )
infixr  200 _∈_```