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

diff zf.agda @ 34:c9ad0d97ce41

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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)