diff zf.agda @ 324:fbabb20f222e

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 04 Jul 2020 18:18:17 +0900
parents 6f10c47e4e7a
children 17adeeee0c2a
line wrap: on
line diff
--- a/zf.agda	Sat Jul 04 12:53:40 2020 +0900
+++ b/zf.agda	Sat Jul 04 18:18:17 2020 +0900
@@ -49,7 +49,7 @@
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
      -- regularity without minimum
-     ε-induction : { ψ : ZFSet → Set (suc m)}
+     ε-induction : { ψ : ZFSet → Set m}
               → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
               → (x : ZFSet ) → ψ x
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )