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

changeset 111:1daa1d24348c

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 Thu, 20 Jun 2019 13:18:18 +0900
parents dab56d357fa3
children c42352a7ee07
files ordinal-definable.agda ordinal.agda zf.agda
diffstat 3 files changed, 38 insertions(+), 113 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Tue Jun 18 23:40:17 2019 +0900
+++ b/ordinal-definable.agda	Thu Jun 20 13:18:18 2019 +0900
@@ -66,7 +66,7 @@
   -- supermum as Replacement Axiom
   sup-o  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-o< : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → ∀ {x : Ordinal {n}} →  ψ x  o<  sup-o ψ 
-  -- a property of supermum required in Power Set Axiom
+  -- contra-position of mimimulity of supermum required in Power Set Axiom
   sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
   -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
@@ -114,11 +114,7 @@
 
 transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z  ∋ x
 transitive  {n} {z} {y} {x} z∋y x∋y  with  ordtrans ( c<→o< {suc n} {x} {y} x∋y ) (  c<→o< {suc n} {y} {z} z∋y ) 
-... | t = lemma0 (lemma t) where
-   lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord x)
-   lemma xo<z = {!!} -- o<→c< xo<z
-   lemma0 :  def ( ord→od ( od→ord z )) ( od→ord x) →  def z (od→ord x)
-   lemma0 dz  = def-subst {suc n} { ord→od ( od→ord z )} { od→ord x} dz (oiso)  refl
+... | t = otrans z z∋y (c<→o< {suc n} {x} {y} x∋y ) 
 
 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
   field
@@ -162,52 +158,11 @@
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
-o<→o> : {n : Level} →  { x y : OD {n} } →  (x == y) → (od→ord x ) o< ( od→ord y) → ⊥
-o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with
-     yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} {!!} oiso refl )
-... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
-... | ()
-o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with
-     yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} {!!} oiso refl )
-... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
-... | ()
-
-==→o≡ : {n : Level} →  { x y : Ordinal {suc n} } → ord→od x == ord→od y →  x ≡ y 
-==→o≡ {n} {x} {y} eq with trio< {n} x y
-==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
-==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
-==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
-
-≡-def : {n : Level} →  { x : Ordinal {suc n} } → x ≡ od→ord (Ord x)
-≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where
-    lemma :  ord→od x == record { def = λ z → z o< x }
-    eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where 
-        t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
-        t = c<→o< {suc n} {ord→od w} {ord→od x} (def-subst {suc n} {_} {_} {ord→od x} {_} z refl (sym diso))
-    eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} {!!} refl refl
-
-od≡-def : {n : Level} →  { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } 
-od≡-def {n} {x} = subst (λ k  → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
-
-==→o≡1 : {n : Level} →  { x y : OD {suc n} } → x == y →  od→ord x ≡ od→ord y 
-==→o≡1 eq = ==→o≡ (subst₂ (λ k j → k == j ) (sym oiso) (sym oiso) eq )
-
-==-def-l : {n : Level } {x y : Ordinal {suc n} } { z : OD {suc n} }→ (ord→od x == ord→od y) → def z x → def z y
-==-def-l {n} {x} {y} {z} eq z>x = subst ( λ k → def z k ) (==→o≡ eq) z>x
-
-==-def-r : {n : Level } {x y : OD {suc n} } { z : Ordinal {suc n} }→ (x == y) → def x z → def y z
-==-def-r {n} {x} {y} {z} eq z>x = subst (λ k → def k z ) (subst₂ (λ j k → j ≡ k ) oiso oiso (cong (λ k → ord→od k) (==→o≡1 eq))) z>x  
-
 ∋→o< : {n : Level} →  { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
 ∋→o< {n} {a} {x} lt = t where
          t : (od→ord x) o< (od→ord a)
          t = c<→o< {suc n} {x} {a} lt 
 
-o<∋→ : {n : Level} →  { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x 
-o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso refl t  where
-         t : def (ord→od (od→ord a)) (od→ord x)
-         t = {!!} -- o<→c< {suc n} {od→ord x} {od→ord a} lt 
-
 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
@@ -222,31 +177,15 @@
 ord-od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
     lemma :  o∅ {suc n } o< (od→ord (Ord (o∅ {suc n}))) → ⊥
     lemma lt with  o<→c< lt
-    lemma lt | t = o<¬≡ _ _ refl t
+    lemma lt | t = o<¬≡ refl t
 ord-od∅ {n} | tri≈ ¬a b ¬c = b
 ord-od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
 
-
-o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
-o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
-
 o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
 
 o≡→¬c< : {n : Level} →  { x y : OD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
-o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) (c<→o< lt) 
-
-tri-c< : {n : Level} →  Trichotomous _==_ (_c<_ {suc n})
-tri-c< {n} x y with trio< {n} (od→ord x) (od→ord y) 
-tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst {!!} oiso refl) (o<→¬== a) ( o<→¬c> a )
-tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b))
-tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst {!!} oiso refl)
-
-c<> : {n : Level } { x y : OD {suc n}} → x c<  y  → y c< x  →  ⊥
-c<> {n} {x} {y} x<y y<x with tri-c< x y
-c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x
-c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> b ( c<→o< x<y )
-c<> {n} {x} {y} x<y y<x | tri> ¬a ¬b c = ¬a x<y
+o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡  (orefl oeq ) (c<→o< lt) 
 
 ∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ ; otrans = λ () } == od∅ {n} 
 eq→ ∅0 {w} (lift ())
@@ -257,18 +196,12 @@
 ∅< {n} {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
 ∅< {n} {x} {y} d eq | lift ()
        
-∅6 : {n : Level} →  { x : OD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
-∅6 {n} {x} x∋x = c<> {n} {x} {x} x∋x x∋x
+-- ∅6 : {n : Level} →  { x : OD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
+-- ∅6 {n} {x} x∋x = c<> {n} {x} {x} x∋x x∋x
 
 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
 def-iso refl t = t
 
-is-∋ : {n : Level} →  ( x y : OD {suc n} ) → Dec ( x ∋ y )
-is-∋ {n} x y with tri-c< x y
-is-∋ {n} x y | tri< a ¬b ¬c = no ¬c
-is-∋ {n} x y | tri≈ ¬a b ¬c = no ¬c
-is-∋ {n} x y | tri> ¬a ¬b c = yes c
-
 is-o∅ : {n : Level} →  ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} )
 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl
 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
@@ -297,6 +230,9 @@
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
     record { def = λ y → osuc y o< (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }) )) ; otrans = {!!} }
 
+omega : { n : Level } → Ordinal {n}
+omega = record { lv = Suc Zero ; ord = Φ 1 }
+
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -308,13 +244,16 @@
     ; Power = Power
     ; Select = Select
     ; Replace = Replace
-    ; infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
+    ; infinite = Ord omega
     ; isZF = isZF 
  } where
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
     Replace X ψ = sup-od ψ
-    Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n}
-    Select X ψ = record { def = λ x →  ( def X  x ∧  ψ ( Ord x )) ; otrans = {!!} } 
+    Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → X ∋ x → Set (suc n) ) → OD {suc n}
+    Select X ψ = record { def = λ x →  ( (d : def X x ) →  ψ (ord→od x) (subst (λ k → def X k ) (sym diso) d)) ; otrans = lemma }  where
+       lemma : {x y : Ordinal} → ((d : def X x) → ψ (ord→od x) (subst (def X) (sym diso) d)) →
+            y o< x → (d : def X y) → ψ (ord→od y) (subst (def X) (sym diso) d)
+       lemma {x} {y} f y<x d = {!!}
     _,_ : OD {suc n} → OD {suc n} → OD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     Union : OD {suc n} → OD {suc n}
@@ -328,7 +267,7 @@
     _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set (suc n)
     _⊆_ A B {x} = A ∋ x →  B ∋ x
     _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ (B ∋ x) )
+    A ∩ B = Select (A , B) (  λ x d → ( A ∋ x ) ∧ (B ∋ x) )
     -- _∪_ : ( A B : ZFSet  ) → ZFSet
     -- A ∪ B = Select (A , B) (  λ x → (A ∋ x)  ∨ ( B ∋ x ) )
     ｛_｝ : ZFSet → ZFSet
@@ -337,7 +276,7 @@
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (Ord omega)
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -379,7 +318,7 @@
               lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 
               lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))  ∋ x
               lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso  )
-              lemma-s | case1 eq = def-subst ( ==-def-r (o≡→== eq) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) ) oiso refl
+              lemma-s | case1 eq = def-subst {!!} oiso refl
               lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst {!!} oiso refl ) t∋x
          -- 
          -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
@@ -393,7 +332,7 @@
               eq← lemma-eq {z} w = record { proj2 = w  ;
                  proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
               lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
-              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (==→o≡1 (lemma-eq))
+              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) {!!}
               lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
               lemma = sup-o<   
          union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z
@@ -412,11 +351,8 @@
          union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
-         selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-         selection {ψ} {X} {y} = record {
-              proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = {!!} } -- ψiso {ψ} (proj2 cond) (sym oiso)  }
-            ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) {!!}  }
-           }
+         selection : {X : OD } {ψ : (x : OD ) →  x ∈ X  → Set (suc n)} {y : OD} → ((d : X ∋ y ) → ψ y d ) ⇔ (Select X ψ ∋ y)
+         selection {ψ} {X} {y} =  {!!}
          replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
          replacement {ψ} X x = sup-c< ψ {x}
          ∅-iso :  {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 
@@ -424,12 +360,11 @@
          minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
          minimul x  not = {!!}
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
-            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ d → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = {!!}
          proj2 (regularity x not ) = record { eq→ = reg ; eq← = {!!} } where
-            reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
-            reg {y} t with proj1 t
-            ... | x∈∅ = {!!}
+            reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ d → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
+            reg {y} t = {!!}
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
@@ -440,34 +375,24 @@
              lemma1 : {x  : OD {suc n}} → od→ord x o< od→ord (x , x)
              lemma1 {x} = c<→o< ( proj1 (pair x x ) )
              lemma2 : {x  : OD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x)
-             lemma2 = trans ( cong ( λ k →  od→ord k ) xx-union ) (sym ≡-def)
+             lemma2 = trans ( cong ( λ k →  od→ord k ) xx-union ) {!!}
              lemma : {x  : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
              lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 )
          uxxx-union : {x  : OD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
          uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) lemma where
              lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
-             lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) (sym ≡-def )
+             lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) {!!}
          uxxx-2 : {x  : OD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) }
          eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt
          eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt
          uxxx-ord : {x  : OD {suc n}} → od→ord (Union (x , (x , x))) ≡ osuc (od→ord x)
-         uxxx-ord {x} = trans (cong (λ k →  od→ord k ) uxxx-union) (==→o≡ (subst₂ (λ j k → j == k ) (sym oiso) (sym od≡-def ) uxxx-2 )) 
-         omega = record { lv = Suc Zero ; ord = Φ 1 }
+         uxxx-ord {x} = trans (cong (λ k →  od→ord k ) uxxx-union) {!!} 
          infinite : OD {suc n}
-         infinite = ord→od ( omega )
-         infinity∅ : ord→od ( omega ) ∋ od∅ {suc n}
-         infinity∅ = def-subst {suc n} {_} {o∅} {infinite} {od→ord od∅}
-              {!!}  refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (cong (λ k →  od→ord k) o∅≡od∅ ))
-         infinite∋x : (x : OD) → infinite ∋ x → od→ord x o< omega
-         infinite∋x x lt = subst (λ k → od→ord x o< k ) diso t where
-              t  : od→ord x o< od→ord (ord→od (omega))
-              t  = ∋→o< {n} {infinite} {x} lt
-         infinite∋uxxx : (x : OD) → osuc (od→ord x) o< omega → infinite ∋ Union (x , (x , x ))
-         infinite∋uxxx x lt = o<∋→ t where
-              t  :  od→ord (Union (x , (x , x))) o< od→ord (ord→od (omega))
-              t  = subst (λ k →  od→ord (Union (x , (x , x))) o< k ) (sym diso ) ( subst ( λ k → k o< omega ) ( sym  (uxxx-ord {x} ) ) lt ) 
+         infinite = Ord omega 
+         infinity∅ : Ord omega  ∋ od∅ {suc n}
+         infinity∅ = {!!}
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x lt = infinite∋uxxx x ( lemma (od→ord x) (infinite∋x x lt ))   where
+         infinity x lt = {!!} where
               lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 
               lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
               lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
--- a/ordinal.agda	Tue Jun 18 23:40:17 2019 +0900
+++ b/ordinal.agda	Thu Jun 20 13:18:18 2019 +0900
@@ -113,9 +113,9 @@
 =→¬< {Zero} ()
 =→¬< {Suc x} (s≤s lt) = =→¬< lt
 
-o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy  → ox o< oy  → ⊥
-o<¬≡ ox ox refl (case1 lt) =  =→¬< lt
-o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
+o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy  → ox o< oy  → ⊥
+o<¬≡ {_} {ox} {ox} refl (case1 lt) =  =→¬< lt
+o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt
 
 ¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
 ¬x<0 {n} {x} (case1 ())
--- a/zf.agda	Tue Jun 18 23:40:17 2019 +0900
+++ b/zf.agda	Thu Jun 20 13:18:18 2019 +0900
@@ -36,7 +36,7 @@
      (_,_ : ( A B : ZFSet  ) → ZFSet)
      (Union : ( A : ZFSet  ) → ZFSet)
      (Power : ( A : ZFSet  ) → ZFSet)
-     (Select : ZFSet → ( ZFSet → Set m ) → ZFSet )
+     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) →  X ∋ x → Set m ) → ZFSet ) 
      (Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet )
      (infinite : ZFSet)
        : Set (suc (n ⊔ m)) where
@@ -53,7 +53,7 @@
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
   _⊆_ A B {x} = A ∋ x →  B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
+  A ∩ B = Select A (  λ x d → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
   A ∪ B = Union (A , B)    -- Select A (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  ) is easer
   ｛_｝ : ZFSet → ZFSet
@@ -74,7 +74,7 @@
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
      infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
-     selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
+     selection : ∀ { X : ZFSet  } →  { ψ : (x : ZFSet ) →  x ∈ X → Set m } → ∀ {  y : ZFSet  } →  ( ( d : y ∈ X ) → ψ y d ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( ψ x ∈  Replace X ψ )  
    -- -- ∀ z [ ∀ x ( x ∈ z  → ¬ ( x ≈ ∅ ) )  ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y )  → x ∩ y ≈ ∅  ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ]
@@ -94,7 +94,7 @@
      _,_ : ( A B : ZFSet  ) → ZFSet
      Union : ( A : ZFSet  ) → ZFSet
      Power : ( A : ZFSet  ) → ZFSet
-     Select : ZFSet → ( ZFSet → Set m ) → ZFSet
+     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) →  X ∋ x → Set m ) → ZFSet 
      Replace : ZFSet → ( ZFSet → ZFSet ) → ZFSet
      infinite : ZFSet
      isZF : IsZF ZFSet _∋_ _≈_ ∅ _,_ Union Power Select Replace infinite