# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1557540653 -32400
# Node ID c12d964a04c06b62afc1687a6a73ee26b5449aa0
# Parent  e7990ff544bfa143a2e1b9783bf1051693052e87
...

diff -r e7990ff544bf -r c12d964a04c0 zf.agda
--- a/zf.agda	Sat May 11 10:47:23 2019 +0900
+++ b/zf.agda	Sat May 11 11:10:53 2019 +0900
@@ -60,15 +60,15 @@
   infixr  230 _∩_ _∪_
   infixr  220 _⊆_ 
   field
-     empty : ( x : ZFSet  ) → ¬ ( ∅ ∋ x )
+     empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
      -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
-     power→ : ( A X t : ZFSet  ) → A ∋ t → ∀ {x} {y} →  _⊆_ t X {x} {y}
-     power← : ( A X t : ZFSet  ) → ∀ {x} {y} →  _⊆_ t X {x} {y} → A ∋ t 
+     power→ : ( A t : ZFSet  ) → Power A ∋ t → ∀ {x} {y} →  _⊆_ t A {x} {y}
+     power← : ( A t : ZFSet  ) → ∀ {x} {y} →  _⊆_ t A {x} {y} → Power A ∋ t 
      -- extentionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extentionality :  ( A B z  : ZFSet  ) → A ∋ z ⇔ B ∋ z → A ≈ B
      -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
-     smaller : ZFSet → ZFSet
-     regularity : ( x : ZFSet  ) → ¬ (x ≈ ∅) → smaller x  ∩ x  ≈ ∅ 
+     -- smaller : ZFSet → ZFSet
+     -- regularity : ( x : ZFSet  ) → ¬ (x ≈ ∅) → smaller x  ∩ x  ≈ ∅ 
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinite : ZFSet
      infinity∅ :  ∅ ∈ infinite