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

comparison cardinal.agda @ 274:29a85a427ed2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ε-induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 25 Apr 2020 15:09:07 +0900
parents 985a1af11bce
children 6f10c47e4e7a
comparison
equal deleted inserted replaced
273:9ccf8514c323 274:29a85a427ed2
3 module cardinal {n : Level } (O : Ordinals {n}) where 3 module cardinal {n : Level } (O : Ordinals {n}) where
4 4
5 open import zf 5 open import zf
6 open import logic 6 open import logic
7 import OD 7 import OD
8 import OPair
8 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) 9 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
9 open import Relation.Binary.PropositionalEquality 10 open import Relation.Binary.PropositionalEquality
10 open import Data.Nat.Properties 11 open import Data.Nat.Properties
11 open import Data.Empty 12 open import Data.Empty
12 open import Relation.Nullary 13 open import Relation.Nullary
14 open import Relation.Binary.Core 15 open import Relation.Binary.Core
15 16
16 open inOrdinal O 17 open inOrdinal O
17 open OD O 18 open OD O
18 open OD.OD 19 open OD.OD
20 open OPair O
19 21
20 open _∧_ 22 open _∧_
21 open _∨_ 23 open _∨_
22 open Bool 24 open Bool
23 open _==_ 25 open _==_