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

comparison 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
comparison
equal deleted inserted replaced
33:2b853472cb24 34:c9ad0d97ce41
30 open import Relation.Binary.Core 30 open import Relation.Binary.Core
31 31
32 infixr 130 _∧_ 32 infixr 130 _∧_
33 infixr 140 _∨_ 33 infixr 140 _∨_
34 infixr 150 _⇔_ 34 infixr 150 _⇔_
35
36 record Func {n m : Level } (ZFSet : Set n) (_≈_ : Rel ZFSet m) : Set (n ⊔ suc m) where
37 field
38 rel : Rel ZFSet m
39 dom : ( y : ZFSet ) → ∀ { x : ZFSet } → rel x y
40 fun-eq : { x y z : ZFSet } → ( rel x y ∧ rel x z ) → y ≈ z
41
42 open Func
43
44 35
45 record IsZF {n m : Level } 36 record IsZF {n m : Level }
46 (ZFSet : Set n) 37 (ZFSet : Set n)
47 (_∋_ : ( A x : ZFSet ) → Set m) 38 (_∋_ : ( A x : ZFSet ) → Set m)
48 (_≈_ : Rel ZFSet m) 39 (_≈_ : Rel ZFSet m)