Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
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) |