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

comparison filter.agda @ 193:0b9645a65542

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 Mon, 29 Jul 2019 08:41:16 +0900
parents 9eb6a8691f02
children 650bdad56729
comparison
equal deleted inserted replaced
192:38ecc75d93ce 193:0b9645a65542
1 open import Level 1 open import Level
2 module filter where 2 open import OD
3
4 open import zf 3 open import zf
5 open import ordinal 4 open import ordinal
6 open import OD 5 module filter ( n : Level ) where
6
7 open import Relation.Nullary 7 open import Relation.Nullary
8 open import Relation.Binary 8 open import Relation.Binary
9 open import Data.Empty 9 open import Data.Empty
10 open import Relation.Binary 10 open import Relation.Binary
11 open import Relation.Binary.Core 11 open import Relation.Binary.Core
12 open import Relation.Binary.PropositionalEquality 12 open import Relation.Binary.PropositionalEquality
13 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 13 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
14
15 od = OD→ZF {n}
14 16
15 17
16 record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where 18 record Filter {n : Level} ( P max : OD {suc n} ) : Set (suc (suc n)) where
17 field 19 field
18 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n) 20 _⊇_ : OD {suc n} → OD {suc n} → Set (suc n)