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

diff zf.agda @ 29:fce60b99dc55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
posturate OD is isomorphic to Ordinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 20 May 2019 18:18:43 +0900
parents 7293a151d949
children 3b0fdb95618e
line wrap: on
line diff
--- a/zf.agda	Sun May 19 18:13:42 2019 +0900
+++ b/zf.agda	Mon May 20 18:18:43 2019 +0900
@@ -55,7 +55,7 @@
      (infinite : ZFSet)
        : Set (suc (n ⊔ m)) where
   field
-     isEquivalence : {A B : ZFSet} → IsEquivalence {n} {m} {ZFSet} _≈_ 
+     isEquivalence : IsEquivalence {n} {m} {ZFSet} _≈_ 
      -- ∀ x ∀ y ∃ z(x ∈ z ∧ y ∈ z)
      pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
      -- ∀ X ∃ A∀ t(t ∈ A ⇔ ∃ x ∈ X(t  ∈ x))