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

diff zf.agda @ 123:0c2cbf37e002

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 Sun, 30 Jun 2019 20:31:10 +0900
parents 47541e86c6ac
children 3849614bef18
line wrap: on
line diff
--- a/zf.agda	Sun Jun 30 11:03:34 2019 +0900
+++ b/zf.agda	Sun Jun 30 20:31:10 2019 +0900
@@ -18,6 +18,7 @@
 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
+
 open import Relation.Nullary
 open import Relation.Binary