Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 34:c9ad0d97ce41
fix oridinal
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 22 May 2019 11:52:49 +0900 |
parents | 3b0fdb95618e |
children | f10ceee99d00 |
line wrap: on
line diff
--- a/zf.agda Tue May 21 18:17:24 2019 +0900 +++ b/zf.agda Wed May 22 11:52:49 2019 +0900 @@ -33,15 +33,6 @@ infixr 140 _∨_ infixr 150 _⇔_ -record Func {n m : Level } (ZFSet : Set n) (_≈_ : Rel ZFSet m) : Set (n ⊔ suc m) where - field - rel : Rel ZFSet m - dom : ( y : ZFSet ) → ∀ { x : ZFSet } → rel x y - fun-eq : { x y z : ZFSet } → ( rel x y ∧ rel x z ) → y ≈ z - -open Func - - record IsZF {n m : Level } (ZFSet : Set n) (_∋_ : ( A x : ZFSet ) → Set m)